Gymbo
1.0.0
O Gymbo é uma prova de conceito para um mecanismo de execução simbólica baseado em gradiente implementado do zero. Com base em avanços recentes que utilizam a descida de gradiente para resolver fórmulas SMT [1, 2] , a gimlia aproveita a ascendência do gradiente para descobrir valores de entrada que atendem a cada restrição de caminho durante a execução simbólica. Para mais informações, consulte nossa documentação.
Comparado a outras ferramentas proeminentes de execução simbólica, a implementação do GyMBO é notavelmente mais simples e mais compacta. Esperamos que este projeto ajude os indivíduos a entender os princípios fundamentais de execução simbólica e solução de problemas de SMT através de descendência de gradiente.
Um uso prático de gymbo é depurar modelos de ML, como redes neurais, para detectar comportamentos inesperados. Por exemplo, você pode gerar exemplos adversários com gymbo convertendo redes neurais em programas imperativos.
Outra característica única do gymbo é que ele pode rastrear as variáveis simbólicas probabilísticas. Adotamos o algoritmo PBRANCH proposto em [3] e atualmente apoiamos as distribuições uniformes discretas, Bernoulli e binomial.
Observe que o Gymbo está atualmente em desenvolvimento e pode ter erros. Seus comentários e contribuições são sempre muito apreciados.
git clone https://github.com/Koukyosyumei/Gymbo.git
./script/build.shConfira alguns exemplos no diretório de exemplo:
Atualmente, o Gymbo suporta programas do tipo C com a seguinte 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 ")"
Observe que o Gymbo atualmente ignora
/ao resolver restrições de caminho.
O Gymbo converte a restrição do caminho em uma função de perda numérica, que se torna negativa somente quando a restrição do caminho é atendida. Gymbo usa a seguinte regra de transformação:
!(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)
Aqui, eps é o menor valor positivo do tipo para a e b.
Por exemplo, quando a e b são inteiros ( eps = 1 ), (a < 3) && (!(a < 3) || (b == 5)) se torna max(a - 2, min(3 - a, abs(b - 5))) .
Opcionalmente, o Gymbo pode usar o DPLL (SAT Solver) para decidir a atribuição para cada termo exclusivo, às vezes resultando em melhor escalabilidade. Por exemplo, aplicar DPLL ao exemplo acima leva a (a < 3) sendo verdadeiro e (b == 5) sendo verdadeiro. O Gymbo então converte essa atribuição em uma função de perda a ser resolvida: max(a - 2, abs(b - 5)) .
O comando gymbo aceita as seguintes opções de linha de comando:
-d : defina a profundidade máxima para a execução simbólica (Padrão: 256).-v : defina o nível de verbosidade (padrão: 1). Use -1 para saída 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 : defina o número de iterações para a descida de gradiente (padrão: 100).-a : defina o tamanho da etapa para a descida de gradiente (padrão: 1.0).-e : defina o EPS para a expressão diferenciável (padrão: 1.0).-t : defina o número máximo de ensaios de descida de gradiente (Padrão: 3)-l : defina o valor mínimo dos parâmetros iniciais (padrão: -10)-h : defina o valor máximo dos parâmetros iniciais (padrão: 10)-s : defina a semente aleatória (padrão: 42)-p : (opcional) Se definido, use DPLL para determinar a atribuição para cada termo. Caso contrário, resolva a função de perda diretamente transformada das restrições do caminho. ./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 somente para cabeçalhoComo o Gymbo consiste na biblioteca somente de cabeçalho, você pode criar facilmente sua própria ferramenta de execução 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 : invólucro python 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 aprendizado de máquina de depuração Oferecemos algumas funções auxiliares na Biblioteca pymlgymbo para converter os modelos ML da famosa biblioteca Python como Sklearn e Pytorch no programa que a Gymbo pode processar.
O código a seguir gera os exemplos adversários em relação a uma rede neural, conforme proposto em [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 ) O Gymbo é totalmente implementado no C ++ e requer apenas bibliotecas padrão. O processo de compilação do código -fonte para as máquinas de pilha é baseado na implementação de rui314/chibicc [5] , enquanto a abordagem de execução simbólica é inspirada em 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
