Gymbo
1.0.0
Gymbo هو دليل على مفهوم محرك تنفيذ رمزي قائم على التدرج المنفذ من نقطة الصفر. بناءً على التطورات الحديثة التي تستخدم نزولًا متدرجًا لحل صيغ SMT [1, 2] ، فإن صالة الألعاب الرياضية تعزز من الهبوط التدريجي لاكتشاف قيم الإدخال التي تفي بكل قيد المسار أثناء التنفيذ الرمزي. لمزيد من المعلومات ، تحقق من وثائقنا.
بالمقارنة مع أدوات التنفيذ الرمزية البارزة الأخرى ، فإن تنفيذ Gymbo أبسط وأكثر إحكاما بشكل ملحوظ. نأمل أن يساعد هذا المشروع الأفراد في استيعاب المبادئ الأساسية للتنفيذ الرمزي وحل SMT من خلال نزول التدرج.
أحد الاستخدامات العملية لصالة الألعاب الرياضية هو تصحيح نماذج ML مثل الشبكات العصبية للكشف عن سلوكيات غير متوقعة. على سبيل المثال ، يمكنك إنشاء أمثلة عدوانية مع Gymbo من خلال تحويل الشبكات العصبية إلى برامج حتمية.
ميزة أخرى فريدة من نوعها في صالة الألعاب الرياضية هي أنه يمكنه تتبع المتغيرات الرمزية الاحتمالية. نعتمد خوارزمية PBRANCH المقترحة في [3] ودعم حاليًا التوزيعات الموحدة المنفصلة ، Bernoulli ، و Binomial.
يرجى ملاحظة أن Gymbo قيد التطوير حاليًا وقد يكون له أخطاء. ملاحظاتك ومساهماتك هي دائما موضع تقدير كبير.
git clone https://github.com/Koukyosyumei/Gymbo.git
./script/build.shتحقق من بعض الأمثلة في دليل المثال:
يدعم Gymbo حاليًا برامج تشبه C مع قواعد BNF التالية:
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 يتجاهل
/عند حل قيود المسار.
يحول صالة الألعاب الرياضية قيود المسار إلى دالة فقدان عددي ، والتي تصبح سلبية فقط عند استيفاء قيود المسار. يستخدم 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 Solver) لتحديد المهمة لكل مصطلح فريد ، مما يؤدي أحيانًا إلى قابلية التوسع بشكل أفضل. على سبيل المثال ، يؤدي تطبيق DPLL على المثال أعلاه إلى (a < 3) أن يكون صحيحًا و (b == 5) يكون صحيحًا. ثم يحول Gymbo هذه المهمة إلى وظيفة خسارة ليتم حلها: 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 : مكتبة رأس فقطنظرًا لأن Gymbo يتكون من مكتبة الرأس فقط ، يمكنك بسهولة إنشاء أداة التنفيذ الرمزية الخاصة بك.
# 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 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 لتحويل نماذج ML من مكتبة Python الشهيرة مثل Sklearn و Pytorch إلى البرنامج الذي يمكن أن يعالجه صالة الألعاب الرياضية.
يولد الرمز التالي أمثلة عدوانية ضد شبكة عصبية ، كما هو مقترح في [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 بالكامل في 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
