Gymbo
1.0.0
ジンボは、ゼロから実装されたグラデーションベースのシンボリック実行エンジンの概念の証明です。勾配降下を利用してSMT式[1, 2]を解決する最近の進歩に基づいて、ジンボは勾配降下を活用して、シンボリック実行中に各パス制約を満たす入力値を発見します。詳細については、ドキュメントを確認してください。
他の顕著な象徴的な実行ツールと比較して、ジムの実装は著しく単純でコンパクトです。このプロジェクトが、象徴的な実行と勾配降下によるSMTの問題解決の基本原則を把握するのに役立つことを願っています。
ジムの実際的な使用の1つは、ニューラルネットワークのようなMLモデルをデバッグして、予期しない動作を検出することです。たとえば、ニューラルネットワークを必須プログラムに変換することにより、ジンボで敵対的な例を生成できます。
ジンボのもう1つのユニークな機能は、確率論的な象徴的変数を追跡できることです。 [3]で提案されているPbranchアルゴリズムを採用し、現在、個別の均一、Bernoulli、および二項分布をサポートしています。
ジンボは現在開発中であり、バグがあるかもしれないことに注意してください。あなたのフィードバックと貢献は常に大歓迎です。
git clone https://github.com/Koukyosyumei/Gymbo.git
./script/build.sh例の例のいくつかの例をご覧ください：
ジンボは現在、次の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 ")"
現在、ジンボはパスの制約を解決するときに
/していることに注意してください。
Gymboは、パスの制約を数値損失関数に変換します。これは、パスの制約が満たされた場合にのみ負になります。ジンボは次の変換ルールを使用します。
!(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)))なります。
オプションで、GymboはDPLL（SATソルバー）を使用して、各一意の用語の割り当てを決定し、場合によってはスケーラビリティが向上する場合があります。たとえば、上記の例にDPLLを適用すると(a < 3)が真であること、 (b == 5)が真であることにつながります。ジンボは、この割り当てを解決する損失関数に変換します： 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 ：ヘッダーのみのライブラリジムはヘッダーのみのライブラリで構成されているため、独自のシンボリック実行ツールを簡単に作成できます。
# 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 ： libgymboのPythonラッパー 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 Library内のヘルパー機能を提供して、SklearnやPytorchなどの有名なPythonライブラリのMLモデルをGymboが処理できるプログラムに変換します。
次のコードは[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 )ジンボは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
