Gymbo
1.0.0
Gymbo es una prueba de concepto para un motor de ejecución simbólica basado en gradiente implementado desde cero. Sobre la base de avances recientes que utilizan descenso de gradiente para resolver las fórmulas SMT [1, 2] , Gymbo aprovecha el descenso de gradiente para descubrir valores de entrada que cumplen cada restricción de ruta durante la ejecución simbólica. Para obtener más información, consulte nuestra documentación.
En comparación con otras herramientas de ejecución simbólica prominentes, la implementación de Gymbo es notablemente más simple y más compacta. Esperamos que este proyecto ayude a las personas a comprender los principios fundamentales de la ejecución simbólica y la resolución de problemas SMT a través del descenso de gradiente.
Un uso práctico de Gymbo es depurar modelos ML como redes neuronales para detectar comportamientos inesperados. Por ejemplo, puede generar ejemplos adversos con Gymbo al convertir las redes neuronales en programas imperativos.
Otra característica única de Gymbo es que puede rastrear las variables simbólicas probabilísticas. Adoptamos el algoritmo PBRANCH propuesto en [3] y actualmente apoyamos las distribuciones discretas uniformes, Bernoulli y binomiales.
Tenga en cuenta que Gymbo está actualmente en desarrollo y puede tener errores. Sus comentarios y contribuciones siempre son muy apreciados.
git clone https://github.com/Koukyosyumei/Gymbo.git
./script/build.shConsulte algunos ejemplos en el directorio de ejemplo:
Gymbo actualmente admite programas similares a C con la siguiente gramática 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 ")"
Tenga en cuenta que Gymbo actualmente ignora
/al resolver restricciones de ruta.
Gymbo convierte la restricción de ruta en una función de pérdida numérica, que se vuelve negativa solo cuando se satisface la restricción de ruta. Gymbo usa la siguiente regla de transformación:
!(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)
Aquí, eps es el valor positivo más pequeño del tipo para A y B.
Por ejemplo, cuando a y b son enteros ( eps = 1 ), (a < 3) && (!(a < 3) || (b == 5)) max(a - 2, min(3 - a, abs(b - 5))) .
Opcionalmente, Gymbo puede usar DPLL (solucionador SAT) para decidir la asignación para cada término único, lo que a veces resulta en una mejor escalabilidad. Por ejemplo, la aplicación de DPLL al ejemplo anterior conduce a que (a < 3) sean verdaderos y (b == 5) sean verdaderos. Gymbo luego convierte esta tarea en una función de pérdida para resolverse: max(a - 2, abs(b - 5)) .
El comando gymbo acepta las siguientes opciones de línea de comandos:
-d : Establezca la profundidad máxima para la ejecución simbólica (predeterminado: 256).-v : Establezca el nivel de verbosidad (predeterminado: 1). Use -1 para una salida mínima. -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 : Establezca el número de iteraciones para el descenso de gradiente (predeterminado: 100).-a : Establezca el tamaño de paso para el descenso de gradiente (predeterminado: 1.0).-e : Establezca el EPS para la expresión diferenciable (predeterminada: 1.0).-t : establezca el número máximo de pruebas de descenso de gradiente (predeterminado: 3)-l : Establezca el valor mínimo de los parámetros iniciales (predeterminado: -10)-h : Establezca el valor máximo de los parámetros iniciales (predeterminado: 10)-s : Establezca la semilla aleatoria (predeterminada: 42)-p : (opcional) Si se establece, use DPLL para determinar la asignación para cada término. De lo contrario, resuelva la función de pérdida directamente transformada de las restricciones de ruta. ./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 : biblioteca solo de encabezadoDado que Gymbo consta de la biblioteca de solo encabezado, puede crear fácilmente su propia herramienta de ejecución simbólica.
# 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 para 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 : modelos de aprendizaje automático de depuración Ofrecemos algunas funciones de ayuda dentro de la biblioteca pymlgymbo para convertir los modelos ML de la famosa biblioteca de Python como Sklearn y Pytorch al programa que el gimnasio puede procesar.
El siguiente código genera los ejemplos adversos contra una red neuronal, como se propuso en [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 se implementa completamente en C ++ y solo requiere bibliotecas estándar. El proceso de compilación del código fuente a las máquinas de pila se basa en la implementación de rui314/chibicc [5] , mientras que el enfoque de ejecución simbólica está inspirado en 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
