Gymbo
1.0.0
Ambobo是从头开始实施的基于梯度的符号执行引擎的概念证明。在最新进步的基础上，利用梯度下降来求解SMT公式[1, 2] ，助理利用梯度下降来发现在符号执行过程中满足每个路径约束的输入值。有关更多信息，请检查我们的文档。
与其他突出的符号执行工具相比，Gymbo的实现非常简单，更紧凑。我们希望该项目将帮助个人掌握符号执行的基本原则和通过梯度下降解决问题的基本原则。
一种实际用途的是锻炼诸如神经网络之类的ML模型，以检测出意外的行为。例如，您可以通过将神经网络转换为当务之急的程序来生成用锻炼的对手示例。
Ambobo的另一个独特功能是它可以跟踪概率符号变量。我们采用[3]中提出的PBranch算法，目前支持离散的统一，Bernoulli和二项式分布。
请注意，Amphbo目前正在开发，可能有错误。您的反馈和贡献总是非常感谢。
git clone https://github.com/Koukyosyumei/Gymbo.git
./script/build.sh在示例目录中查看一些示例：
Ambobo目前通过以下BNF语法支持类似C的程序：
program = stmt*
stmt = expr ";"
| "{" stmt* "}"
| "if" "(" expr ")" stmt ("else" stmt)?
| "return" expr ";"
expr = assign
assign = logical ("=" assign)?
logical = equality ("&&" equality | "||" equality)*
equality = relational ("==" relational | "!=" relational)*
relational = add ("<" add | "<=" add | ">" add | ">=" add)*
add = mul ("+" mul | "-" mul)*
mul = unary ("*" unary | "/" unary)*
unary = ("+" | "-")? primary
primary = num | ident | "(" expr ")"
请注意，当目前忽略
/解决路径约束时。
Amerbo将路径约束转换为数值损耗函数，仅当满足路径约束时，该损失函数才会变为负。体育馆使用以下转换规则：
!(a) => -a + eps
(a < b) => a - b + eps
(a <= b) => a - b
(a > b) => b - a + eps
(a >= b) => b - a
(a == b) => abs(a - b)
(a != b) => -abs(a - b) + eps
(a && b) => max(a, b)
(a || b) => min(a, b)
在这里， eps是A和B类型的最小正值。
例如，当a和b是整数（ eps = 1 ）时， (a < 3) && (!(a < 3) || (b == 5))变为max(a - 2, min(3 - a, abs(b - 5))) 。
可选地，Ambo可以使用DPLL（SAT求解器）来决定每个唯一术语的分配，有时会导致更好的可扩展性。例如，将DPLL应用于上面的示例会导致(a < 3)为真， (b == 5)为true。然后，足体将该任务转换为要解决的损失函数： max(a - 2, abs(b - 5)) 。
gymbo命令接受以下命令行选项：
-d ：设置符号执行的最大深度（默认值：256）。-v ：设置详细级别（默认值：1）。使用-1来最小输出。 -1: the number of satisfiable path constraints and unsatisfiable path constraints.
0: + the list of unique unsatisfiable path constraints.
1: + estimated concrete parameters for each path constraint.
2: + trace at each operation, including the content of the virtual stack and memory.
3: + complete stack machine.
-i ：设置梯度下降的迭代次数（默认值：100）。-a ：设置梯度下降的步长（默认值：1.0）。-e ：设置可区分表达式的EPS（默认：1.0）。-t ：设置梯度下降的最大试验数（默认值：3）-l ：设置初始参数的最小值（默认值：-10）-h ：设置初始参数的最大值（默认值：10）-s ：设置随机种子（默认：42）-p ：（可选）如果设置，请使用DPLL确定每个项的分配。否则，求解从路径约束直接转换的损耗函数。 ./gymbo " if (a < 3) if (a > 4) return 1; " -v 0
> Compiling the input program...
> Start Symbolic Execution...
> ---------------------------
> Result Summary
> # Total Path Constraints: 4
> # SAT: 3
> # UNSAT: 1
> List of UNSAT Path Constraints
> # var_1 < 3 and 4 < var_1 and 1 
libgymbo ：仅标题图书馆由于Amphbo由仅标题库组成，因此您可以轻松地创建自己的符号执行工具。
# include " libgymbo/compiler.h "
# include " libgymbo/gd.h "
# include " libgymbo/parser.h "
# include " libgymbo/tokenizer.h "
# include " libgymbo/type.h "
char user_input[] = " if (a < 3) return 1; "
std::vector<gymbo::Node *> code;
gymbo::Prog prg;
gymbo::GDOptimizer optimizer (num_itrs, step_size);
gymbo::SymState init;
// tokenize the input source code
gymbo::Token *token = gymbo::tokenize(user_input);
// generate AST from the tokens
gymbo::generate_ast (token, user_input, code);
// construct virtual stack machine from AST
gymbo::compile_ast (code, prg);
// execute gradient-based symbolie execution
gymbo::SExecutor executor (optimizer, maxSAT, maxUNSAT, max_num_trials,
ignore_memory, use_dpll, verbose_level);
executor.run(prg, target_pcs, init, max_depth); pip install git+https://github.com/Koukyosyumei/Gymbo
pylibgymbo ：python包装器的libgymbo import pylibgymbo as plg
inp = "a = 1; if (a == 1) return 2;"
var_counter , prg = plg . gcompile ( inp )
optimizer = plg . GDOptimizer ( num_itrs , step_size , ...)
executor = plg . SExecutor ( optimizer , maxSAT , maxUNSAT , max_num_trials ,
ignore_memory , use_dpll , verbose_level )
executor . run ( prg , target_pcs , init , max_depth )pymlgymbo ：调试机器学习模型我们在pymlgymbo库中提供了一些辅助功能，以将著名的Python库的ML模型（如Sklearn和Pytorch）转换为Amberbo可以处理的程序。
如[4]中提出的那样，以下代码针对神经网络生成了对抗性示例。
from sklearn . neural_network import MLPClassifier
import pylibgymbo as plg
import pymlgymbo as pmg
clf = MLPClassifier ( activation = "relu" )
clf . fit ( X_train , y_train )
mlp_code = pmg . dump_sklearn_MLP ( clf , feature_names )
adv_condition = (
"("
+ " || " . join (
[ f"(y_ { c } > y_ { y_pred } )" for c in range ( len ( clf . classes_ )) if y_pred != c ]
)
+ ")"
)
optimizer = plg . GDOptimizer ( num_itrs , step_size , ...)
var_counter , prg = plg . gcompile ( mlp_code )
executor = plg . SExecutor ( optimizer , maxSAT , maxUNSAT , max_num_trials ,
ignore_memory , use_dpll , verbose_level )
executor . run ( prg , target_pcs , init , max_depth )Amphbo完全在C ++中实现，仅需要标准库。从源代码到堆栈计算机编译的过程基于rui314/chibicc [5]的实现，而符号执行方法则受beala/symbolic [6]的启发。
- [1] Chen, Peng, Jianzhong Liu, and Hao Chen. "Matryoshka: fuzzing deeply nested branches." Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. 2019.
- [2] Minghao Liu, Kunhang Lv, Pei Huang, Rui Han, Fuqi Jia, Yu Zhang, Feifei Ma, Jian Zhang. "NRAgo: Solving SMT(NRA) Formulas with Gradient-based Optimization." IEEE/ACM International Conference on Automated Software Engineering, 2023
- [3] Susag, Zachary, et al. "Symbolic execution for randomized programs." Proceedings of the ACM on Programming Languages 6.OOPSLA2 (2022): 1583-1612.
- [4] Gopinath, Divya, et al. "Symbolic execution for importance analysis and adversarial generation in neural networks." 2019 IEEE 30th International Symposium on Software Reliability Engineering (ISSRE). IEEE, 2019.
- [5] https://github.com/rui314/chibicc
- [6] https://github.com/beala/symbolic
