Gymbo
1.0.0
Gymbo est une preuve de concept pour un moteur d'exécution symbolique basé sur un gradient implémenté à partir de zéro. S'appuyant sur les progrès récents qui utilisent une descente de gradient pour résoudre les formules SMT [1, 2] , le gymbo exploite la descente de gradient pour découvrir les valeurs d'entrée qui remplissent chaque contrainte de chemin pendant l'exécution symbolique. Pour plus d'informations, consultez notre documentation.
Par rapport à d'autres outils d'exécution symboliques proéminents, la mise en œuvre de Gymbo est notamment plus simple et plus compacte. Nous espérons que ce projet aidera les individus à saisir les principes fondamentaux de l'exécution symbolique et de la résolution de problèmes SMT par descente de gradient.
Une utilisation pratique de Gymbo est de déboguer des modèles ML comme les réseaux de neurones pour détecter les comportements inattendus. Par exemple, vous pouvez générer des exemples contradictoires avec Gymbo en convertissant les réseaux de neurones en programmes impératifs.
Une autre caractéristique unique de Gymbo est qu'il peut suivre les variables symboliques probabilistes. Nous adoptons l'algorithme PBRANCH proposé dans [3] et soutenons actuellement les distributions uniformes discrètes, Bernoulli et Binomial.
Veuillez noter que Gymbo est actuellement en cours de développement et peut avoir des insectes. Vos commentaires et contributions sont toujours grandement appréciés.
git clone https://github.com/Koukyosyumei/Gymbo.git
./script/build.shConsultez quelques exemples dans l'exemple de répertoire:
Gymbo soutient actuellement les programmes de type C avec la grammaire BNF suivante:
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 ")"
Veuillez noter que Gymbo ignore actuellement
/lors de la résolution des contraintes de chemin.
Gymbo convertit la contrainte de chemin en une fonction de perte numérique, qui ne devient négative que lorsque la contrainte de chemin est satisfaite. Gymbo utilise la règle de transformation suivante:
!(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)
Ici, eps est la plus petite valeur positive du type pour a et b.
Par exemple, lorsque a et b sont des entiers ( eps = 1 ), (a < 3) && (!(a < 3) || (b == 5)) devient max(a - 2, min(3 - a, abs(b - 5))) .
Facultativement, Gymbo peut utiliser DPLL (solveur SAT) pour décider de l'affectation pour chaque terme unique, ce qui entraîne parfois une meilleure évolutivité. Par exemple, l'application de DPLL à l'exemple ci-dessus conduit (a < 3) être vrai et (b == 5) être vrai. Gymbo convertit ensuite cette affectation en une fonction de perte à résoudre: max(a - 2, abs(b - 5)) .
La commande gymbo accepte les options de ligne de commande suivantes:
-d : Définissez la profondeur maximale pour l'exécution symbolique (par défaut: 256).-v : définissez le niveau de verbosité (par défaut: 1). Utilisez -1 pour une sortie minimale. -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 : Définissez le nombre d'itérations pour la descente de gradient (par défaut: 100).-a : Définissez la taille de l'étape pour la descente du gradient (par défaut: 1.0).-e : Définissez l'EPS pour l'expression différenciable (par défaut: 1.0).-t : Définissez le nombre maximum d'essais de descente de gradient (par défaut: 3)-l : définissez la valeur minimale des paramètres initiaux (par défaut: -10)-h : Définissez la valeur maximale des paramètres initiaux (par défaut: 10)-s : Définissez la graine aléatoire (par défaut: 42)-p : (Facultatif) Si défini, utilisez DPLL pour déterminer l'affectation pour chaque terme. Sinon, résolvez la fonction de perte directement transformée à partir des contraintes de chemin. ./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 : bibliothèque d'en-tête uniquementÉtant donné que Gymbo se compose de la bibliothèque d'en-tête uniquement, vous pouvez facilement créer votre propre outil d'exécution symbolique.
# 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 : wrapper python pour 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 : débogage de modèles d'apprentissage automatique Nous proposons des fonctions d'assistance au sein de la bibliothèque pymlgymbo pour convertir les modèles ML de la célèbre bibliothèque Python comme Sklearn et Pytorch au programme que Gymbo peut traiter.
Le code suivant génère les exemples contradictoires contre un réseau neuronal, comme proposé dans [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 est entièrement implémenté en C ++ et ne nécessite que des bibliothèques standard. Le processus de compilation du code source aux machines de pile est basé sur la mise en œuvre de rui314/chibicc [5] , tandis que l'approche d'exécution symbolique est inspirée de 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
