Gymbo
1.0.0
Gymbo ist ein Proof of Concept für eine von Grund auf implementierte Gradienten-basierte symbolische Ausführungsmaschine. Aufbauend auf den jüngsten Fortschritten, bei denen der Gradientenabstieg verwendet wird, um SMT -Formeln zu lösen [1, 2] , nutzt Gymbo den Gradientenabstieg, um Eingabeteile zu entdecken, die jede Pfadbeschränkung während der symbolischen Ausführung erfüllen. Weitere Informationen finden Sie in unserer Dokumentation.
Im Vergleich zu anderen prominenten symbolischen Ausführungswerkzeugen ist die Implementierung von Gymbo besonders einfacher und kompakter. Wir hoffen, dass dieses Projekt Einzelpersonen beim Greifen der grundlegenden Prinzipien der symbolischen Ausführung und der SMT-Problemlösung durch Gradientenabstieg unterstützen wird.
Eine praktische Verwendung von Gymbo ist das Debuggen von ML -Modellen wie neuronale Netze, um unerwartete Verhaltensweisen zu erkennen. Beispielsweise können Sie mit Gymbo kontroverse Beispiele erstellen, indem Sie neuronale Netzwerke in imperative Programme umwandeln.
Ein weiteres einzigartiges Merkmal von Gymbo ist, dass es die probabilistischen symbolischen Variablen verfolgen kann. Wir übernehmen den in [3] vorgeschlagenen Pbranch -Algorithmus und unterstützen derzeit die diskreten Verteilungen der Uniform-, Bernoulli- und Binomialverteilung.
Bitte beachten Sie, dass Gymbo derzeit in der Entwicklung ist und möglicherweise Fehler aufweist. Ihr Feedback und Ihre Beiträge werden immer sehr geschätzt.
git clone https://github.com/Koukyosyumei/Gymbo.git
./script/build.shSchauen Sie sich einige Beispiele im Beispielverzeichnis an:
Gymbo unterstützt derzeit C-ähnliche Programme mit der folgenden BNF-Grammatik:
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 ")"
Bitte beachten Sie, dass Gymbo derzeit ignoriert
/beim Lösen von Pfadbeschränkungen.
Gymbo verwandelt die Pfadbeschränkung in eine numerische Verlustfunktion, die nur dann negativ wird, wenn die Pfadbeschränkung erfüllt ist. Gymbo verwendet die folgende Transformationsregel:
!(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)
Hier ist eps der kleinste positive Wert des Typs für a und b.
Wenn beispielsweise a und b Ganzzahlen sind ( eps = 1 ), wird (a < 3) && (!(a < 3) || (b == 5)) max(a - 2, min(3 - a, abs(b - 5))) .
Optional kann Gymbo verwenden DPLL (SAT Solver), um die Zuordnung für jeden einzigartigen Begriff zu entscheiden, was manchmal zu einer besseren Skalierbarkeit führt. Beispielsweise führt das Anwenden von DPLL auf das obige Beispiel dazu, dass (a < 3) wahr ist und (b == 5) wahr ist. Gymbo wandelt dann diese Zuordnung in eine zu gelöste Verlustfunktion um: max(a - 2, abs(b - 5)) .
Der Befehl gymbo akzeptiert die folgenden Befehlszeilenoptionen:
-d : Stellen Sie die maximale Tiefe für die symbolische Ausführung fest (Standard: 256).-v : Setzen Sie die Ausführungsstufe (Standard: 1). Verwenden Sie -1 für minimale Ausgabe. -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 : Legen Sie die Anzahl der Iterationen für den Gradientenabstieg fest (Standard: 100).-a : Setzen Sie die Schrittgröße für Gradientenabfälle (Standard: 1.0).-e : Setzen Sie das EPS für den differenzierbaren Ausdruck (Standard: 1.0).-t : Setzen Sie die maximale Anzahl von Versuchen mit Gradientenabstieg (Standardeinstellung: 3)-l : Setzen Sie den Mindestwert der Anfangsparameter (Standard: -10)-h : Setzen Sie den Maximalwert der Anfangsparameter (Standardeinstellung: 10)-s : Setzen Sie den zufälligen Saatgut (Standard: 42)-p : (Optional) Wenn festgelegt wird, bestimmen Sie DPLL, um die Zuordnung für jeden Term zu bestimmen. Lösen Sie ansonsten die Verlustfunktion, die direkt aus den Pfadbeschränkungen transformiert ist. ./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 : Nur-Header-BibliothekDa Gymbo aus der nur aus der Header-Bibliothek bestehenden Bibliothek besteht, können Sie problemlos Ihr eigenes symbolisches Ausführungswerkzeug erstellen.
# 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 für 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 : Modelle für maschinelles Lernen debuggen Wir bieten einige Helferfunktionen in pymlgymbo -Bibliothek an, um die ML -Modelle der berühmten Python -Bibliothek wie Sklearn und Pytorch in das Programm umzuwandeln, das Gymbo verarbeiten kann.
Der folgende Code generiert die kontroversen Beispiele gegen ein neuronales Netzwerk, wie in [4] vorgeschlagen.
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 ist vollständig in C ++ implementiert und erfordert nur Standardbibliotheken. Der Prozess des Kompilierens von Quellcode zu Stapelmaschinen basiert auf der Implementierung von rui314/chibicc [5] , während der symbolische Ausführungsansatz von 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
