[开源] 新的 SAT 求解器
Satellite
全新 SAT 求解器喵
技术栈
- CUDA C++
- RUST
- PYTHON + JUPYTER
功能
- 高度可自定义的外部语言约束
- VSCode Extension
- GPU 运算
- 现代化 CDCL
- 分布式计算
适用场景
- 复杂可满足性公式求解
- 机构拥有共享大型机计算资源
- 二进制工程（见下文
安装方法
直接 cargo install satellite-cli 即可使用大部分 cli 功能
如需 vscode extension 可自己编译
python 扩展同理 暂时没有发布至 PyPi
优势
- GPU 加速计算
- 无锁数据结构
- 自动推导 batch dim
- 支持外部约束
- 高性能缓存
二进制工程...?
此求解器可用于移除 denuvo drm
已测试 破解器代码永远不会发出
denuvo 对性能影响约为 2~5%
具体原理是:
先通过 llvm lift 提升并展开动态链接 并 o3+trition pass
然后探测 syscall 网络调用 提取上下文并构建 url 过滤 denuvo 认证服务器调用 标记
接着构建 sat 图树 ast 分析 构建 anti-crash 断言 标记认证链路为不可达 (nop)
运行 satellite 求解
将条件应用回 ir 运行 o3+trition pass
剔除 watchdog 进程 特征是注册大量崩溃处理和 vmcall
dump 并 llvm 编译