HeyGap's_Blog

这篇论文就两页，正好 FM 领域做的人不多，这篇经典论文貌似没被翻译，所以做一下翻译工作，正好夯实一下自己在这个领域的语言基础 摘要    作者提出了一种“允许用户与 Isabelle 服务器进行递进式交互”的环境。在这种环境的帮助下，作者深挖 Isabelle 标准库和形式化证明存档（AFP）并从中提取了 183K 条引理(lemmas)与定理(theorems)。作者还在这样大规模的语料库下训练了大语言模型并展示了他们在证明 AFP 定理的有效性。 介绍    近来“将机器学习模型应用于定理证明”之风盛行。[3,6-8,12,14]等论文都展示了用机器学习模型证明新定理的希望。在本工作中，作者提出挖掘被 Isabelle ITP 使用的库，即 Isabelle 标准库和 AFP。之前研究者已经从标准库和 AFP 中提取数据，用手工设计的特征来训练推荐系统，从而帮助用户选择证明方法。    总而言之，作者做出了以下贡献： 构建了一套agents能以渐进方式与 Isabelle 定理证明器交互的环境。这使得...

夏令营机试笔记 algorithm 库 1234567// 反转vector<T> vec;reverse(vec.begin(), vec.end());// 交换vector<T> vec;swap(vec[1], vec[2]); 数组 基本数据结构 vector 初始化 1234567891011121314using namespace std;vector<int> vec1;vector<int> vec2(5);vector<int> vec3(5,10);vector<int> vec4 = {1,2,3,4,5};vector<int> vec_4{1,2,3,4,5};vector<int> vec5(vec4);vector<int> vec6(vec4.begin(), vec4.end());int arr[] =...

Linux Kernel Pwn 环境搭建与题目复现 环境搭建 qemu busybox busybox 官网 12345678wget https://busybox.net/downloads/busybox-1.37.0.tar.bz2tar -xjf busybox-1.37.0.tar.bz2cd busybox-1.37.0make menuconfig# 将 Settings-Build Options-Build static binary(no shared libs)选中，将Settings-Installation Options-What kind of ... 中的 ./install 改为 ./rootfsmake -j$(nproc) && make install 即可安装cp rootfs/ -r ..# 然后就可以 rm -rf busybox-1.37.0（可选） 内核编译 linux kernel pub 首先使用 file bzImage 查看使用的...

正好要分享一篇论文，所以做一下翻译工作 摘要    GPU 称为现代计算基础设施中不可或缺的一部分。他们在大规模数据集上执行大量的并行任务，并且在 3D 渲染和常规目的并行编程方面有丰富的用户层可接触的 APIs。不幸的是，桥接 API 和 底层硬件 的 GPU 驱动体积正变得越来越庞大且复杂，许多 GPU 驱动暴露了大面积的攻击面并且有非常严重的安全风险。    经过验证，Fuzzing 是一种通过发现潜在漏洞从而缓解安全风险的自动化测试方法。然而，当应用到 GPU 驱动时，现有的 fuzzer 开销较大，并且因为依赖物理GPU从而导致规模性不佳。此外，它们的效果也不是很好，因为在生成输入事件时往往难以满足依赖性和时间上的限制要求。    我们提出了 Moneta，这是一种新的 ex-vivo 驱动程序 fuzzing 方法，可以有状态地、有效地大规模 fuzz GPU 驱动程序。核心思想是① 通过协同结合 snapshot-and-rehost 和 record-and-replay  与我们提出的 GPU 栈虚拟化和...

...

...

...

就像做 pwn 要读 glibc 源码，做 blockchain 怎么能不分析 openzeppelin 呢 [1] ERC20 ERC20 是以太坊上最基本的代币规范 openzeppelin ERC20 源码在这 以下是该合约的变量 123456mapping(address account => uint256) private _balances; // account 该 token 的余额// account 批准 spender 使用的余额，实际上花的还是 account 的 tokensmapping(address account => mapping(address spender => uint256)) private _allowances; uint256 private _totalSupply; // 该合约总共发行的 token 数string private _name; // 该 token 的 namestring private _symbol; // 简约版的...

学习一下 Uniswap V2 [1] 前置知识 [1-1] AMM(Automated Market Makers) 一种去中心化的交易协议，用于在区块链网络中实现无需订单簿的资产交换。传统交易所通常依赖于买家和卖家通过订单簿来匹配交易，而AMM通过智能合约和算法自动确定资产的价格，从而进行交易。 AMM的基本原理是通过池子（Liquidity Pools）来提供流动性。流动性池通常由两种或更多种资产组成，并由流动性提供者（LP）存入这些资产。然后，AMM使用特定的算法（例如常见的x * y...

单一漏洞 + 污点分析做到顶会，暑假就想复现了结果拖到现在 年份：2024 [1] Abstract 基于目前研究较少的address verification漏洞，本文用污点分析实现了的“轻量级”专属扫描工具AVVerifier，检查了数百万的合约，找到了数百个有该漏洞的合约，并将其部署在链上成为实时检测工具，并成功检测到了一次数十万美元的攻击 [2] Intro & Background [2-1] Ethreum Primer 大概讲了一下现在区块链非常火，自从以太坊和智能合约出现后，DApps的各种应用层出不穷，比如闪电贷等。指出为了防止漏报带来的经济损失，能保证soundness的静态符号执行常常被用到（mythril） [2-2] Whitelist address verification Beosin. Two vulnerabilities in one function: The analysis of visor finance exploit....