Gymbo
1.0.0
Gymbo является доказательством концепции для символического движения символического выполнения, основанного на градиенте, реализованного с нуля. Опираясь на недавние достижения, которые используют градиентный спуск для решения формул SMT [1, 2] , гимнологическое расстояние использует градиентный спуск, чтобы обнаружить входные значения, которые выполняют каждое ограничение пути во время символического выполнения. Для получения дополнительной информации проверьте нашу документацию.
По сравнению с другими выдающимися инструментами символического выполнения, реализация Gymbo особенно проще и компактна. Мы надеемся, что этот проект поможет людям в том, чтобы понять фундаментальные принципы символического исполнения и решения проблем SMT через градиентное происхождение.
Одним из практических использования гимно -гимнатора является отладка моделей ML, таких как нейронные сети для обнаружения неожиданного поведения. Например, вы можете генерировать состязательные примеры с гимнологическим обеспечением путем преобразования нейронных сетей в императивные программы.
Еще одна уникальная особенность гимбола заключается в том, что он может отслеживать вероятностные символические переменные. Мы принимаем алгоритм Pbranch, предложенный в [3] , и в настоящее время поддерживают дискретную форму, Бернулли и биномиальные распределения.
Обратите внимание, что Gymbo в настоящее время находится в стадии разработки и может иметь ошибки. Ваши отзывы и вклад всегда высоко ценится.
git clone https://github.com/Koukyosyumei/Gymbo.git
./script/build.shПроверьте несколько примеров в каталоге примера:
Гимбо, в настоящее время поддерживает C-подобные программы со следующей грамматикой 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 использует следующее правило трансформации:
!(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 : библиотека только для заголовковПоскольку гимбо состоит из библиотеки только для заголовков, вы можете легко создать свой собственный инструмент символического выполнения.
# 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 purper для 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 ) Гимбо полностью реализован в 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
