Gymbo
1.0.0
Gymbo เป็นหลักฐานของแนวคิดสำหรับเอ็นจิ้นการดำเนินการเชิงสัญลักษณ์ที่ใช้การไล่ระดับสีตั้งแต่เริ่มต้น การสร้างความก้าวหน้าล่าสุดที่ใช้การไล่ระดับสีเพื่อแก้สูตร SMT [1, 2] , ยิมโทรใช้ประโยชน์จากการไล่ระดับสีเพื่อค้นหาค่าอินพุตที่เติมเต็มข้อ จำกัด ของเส้นทางแต่ละเส้นทางในระหว่างการดำเนินการเชิงสัญลักษณ์ สำหรับข้อมูลเพิ่มเติมตรวจสอบเอกสารของเรา
เมื่อเปรียบเทียบกับเครื่องมือการดำเนินการเชิงสัญลักษณ์ที่โดดเด่นอื่น ๆ การใช้งานของ Gymbo นั้นง่ายกว่าและกะทัดรัดมากขึ้น เราหวังว่าโครงการนี้จะช่วยให้บุคคลในการเข้าใจหลักการพื้นฐานของการดำเนินการเชิงสัญลักษณ์และการแก้ปัญหา SMT ผ่านการสืบเชื้อสายการไล่ระดับสี
การใช้งานที่ใช้งานได้จริงของ Gymbo คือการดีบักรุ่น ML เช่นเครือข่ายประสาทเพื่อตรวจจับพฤติกรรมที่ไม่คาดคิด ตัวอย่างเช่นคุณสามารถสร้างตัวอย่างที่เป็นปฏิปักษ์กับ Gymbo โดยการแปลงเครือข่ายประสาทเป็นโปรแกรมที่จำเป็น
คุณสมบัติที่เป็นเอกลักษณ์อีกอย่างหนึ่งของ Gymbo คือสามารถติดตามตัวแปรสัญลักษณ์ความน่าจะเป็น เราใช้อัลกอริทึม PBRANCH ที่เสนอใน [3] และปัจจุบันสนับสนุนเครื่องแบบที่ไม่ต่อเนื่อง Bernoulli และการแจกแจงแบบทวินาม
โปรดทราบว่า Gymbo กำลังอยู่ระหว่างการพัฒนาและอาจมีข้อบกพร่อง ความคิดเห็นและการมีส่วนร่วมของคุณได้รับการชื่นชมอย่างมากเสมอ
git clone https://github.com/Koukyosyumei/Gymbo.git
./script/build.shตรวจสอบตัวอย่างบางส่วนในไดเรกทอรีตัวอย่าง:
ปัจจุบัน Gymbo รองรับโปรแกรม C-like ด้วยไวยากรณ์ 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 แปลงข้อ จำกัด เส้นทางเป็นฟังก์ชันการสูญเสียตัวเลขซึ่งกลายเป็นลบเฉพาะเมื่อข้อ จำกัด เส้นทางเป็นที่พอใจ 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 : Python wrapper สำหรับ 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 เป็นโปรแกรมที่ 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 ) 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
