Gymbo
1.0.0
Gymbo adalah bukti konsep untuk mesin eksekusi simbolik berbasis gradien yang diimplementasikan dari awal. Membangun kemajuan terbaru yang memanfaatkan keturunan gradien untuk menyelesaikan rumus SMT [1, 2] , Gymbo memanfaatkan keturunan gradien untuk menemukan nilai -nilai input yang memenuhi setiap kendala jalur selama eksekusi simbolik. Untuk informasi lebih lanjut, periksa dokumentasi kami.
Dibandingkan dengan alat eksekusi simbolik terkemuka lainnya, implementasi Gymbo sangat sederhana dan lebih kompak. Kami berharap bahwa proyek ini akan membantu individu dalam memahami prinsip-prinsip dasar pelaksanaan simbolik dan pemecahan masalah SMT melalui keturunan gradien.
Salah satu penggunaan praktis dari Gymbo adalah men -debug model ML seperti jaringan saraf untuk mendeteksi perilaku yang tidak terduga. Misalnya, Anda dapat menghasilkan contoh -contoh permusuhan dengan Gymbo dengan mengubah jaringan saraf menjadi program yang imperatif.
Fitur unik lainnya dari Gymbo adalah dapat melacak variabel simbolis probabilistik. Kami mengadopsi algoritma PBRanch yang diusulkan dalam [3] dan saat ini mendukung distribusi seragam diskrit, Bernoulli, dan binomial.
Harap dicatat bahwa Gymbo saat ini sedang dalam pengembangan dan mungkin memiliki bug. Umpan balik dan kontribusi Anda selalu sangat dihargai.
git clone https://github.com/Koukyosyumei/Gymbo.git
./script/build.shLihatlah beberapa contoh di Direktori Contoh:
Gymbo saat ini mendukung program seperti C dengan tata bahasa BNF berikut:
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 ")"
Harap dicatat bahwa Gymbo saat ini mengabaikan
/saat menyelesaikan kendala jalur.
Gymbo mengubah batasan jalan menjadi fungsi kerugian numerik, yang menjadi negatif hanya ketika kendala jalur dipenuhi. Gymbo menggunakan aturan transformasi berikut:
!(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)
Di sini, eps adalah nilai positif terkecil dari jenis untuk A dan B.
Misalnya, ketika a dan b adalah bilangan bulat ( eps = 1 ), (a < 3) && (!(a < 3) || (b == 5)) menjadi max(a - 2, min(3 - a, abs(b - 5))) .
Secara opsional, Gymbo dapat menggunakan DPLL (SAT Solver) untuk memutuskan tugas untuk setiap istilah unik, kadang -kadang menghasilkan skalabilitas yang lebih baik. Misalnya, menerapkan DPLL ke contoh di atas mengarah pada (a < 3) menjadi benar dan (b == 5) menjadi benar. Gymbo kemudian mengubah tugas ini menjadi fungsi kerugian untuk diselesaikan: max(a - 2, abs(b - 5)) .
Perintah gymbo menerima opsi baris perintah berikut:
-d : Tetapkan kedalaman maksimum untuk eksekusi simbolik (default: 256).-v : Atur level verbositas (default: 1). Gunakan -1 untuk output minimal. -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 : Tetapkan jumlah iterasi untuk keturunan gradien (default: 100).-a : Atur ukuran langkah untuk keturunan gradien (default: 1.0).-e : Atur EPS untuk ekspresi yang dapat dibedakan (default: 1.0).-t : Tetapkan jumlah maksimum uji coba keturunan gradien (default: 3)-l : Atur nilai minimum parameter awal (default: -10)-h : Tetapkan nilai maksimum parameter awal (default: 10)-s : Atur seed acak (default: 42)-p : (opsional) Jika diatur, gunakan DPLL untuk menentukan penugasan untuk setiap istilah. Jika tidak, selesaikan fungsi kerugian yang secara langsung ditransformasikan dari kendala jalur. ./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 : perpustakaan header sajaKarena Gymbo terdiri dari perpustakaan header saja, Anda dapat dengan mudah membuat alat eksekusi simbolik Anda sendiri.
# 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 : Pembungkus Python untuk 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 : Model Pembelajaran Mesin Debugging Kami menawarkan beberapa fungsi pembantu dalam perpustakaan pymlgymbo untuk mengonversi model ML perpustakaan Python yang terkenal seperti Sklearn dan Pytorch ke program yang dapat diproses oleh Gymbo.
Kode berikut menghasilkan contoh permusuhan terhadap jaringan saraf, seperti yang diusulkan dalam [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 ) Gymbo sepenuhnya diimplementasikan di C ++ dan hanya membutuhkan perpustakaan standar. Proses penyusunan dari kode sumber ke mesin stack didasarkan pada implementasi rui314/chibicc [5] , sedangkan pendekatan eksekusi simbolik diilhami oleh 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
