Gymbo
1.0.0
Gymbo는 처음부터 구현 된 그라디언트 기반 상징적 실행 엔진의 개념 증명입니다. Gymbo는 SMT 공식을 해결하기 위해 기울기 하강을 활용하는 최근의 발전을 바탕으로 [1, 2] , Gradient Descent를 활용하여 기호 실행 중 각 경로 제약 조건을 충족시키는 입력 값을 발견합니다. 자세한 내용은 문서를 확인하십시오.
다른 저명한 상징적 실행 도구와 비교할 때 Gymbo의 구현은 더 단순하고 더 컴팩트합니다. 우리는이 프로젝트가 개인이 기호 실행의 기본 원칙을 파악하고 그라디언트 하강을 통해 SMT 문제 해결의 기본 원칙을 파악하는 데 도움이되기를 바랍니다.
Hymbo의 실질적인 사용은 신경망과 같은 ML 모델을 디버깅하여 예상치 못한 행동을 감지하는 것입니다. 예를 들어, 신경망을 명령 프로그램으로 변환하여 Gymbo로 적대적인 예제를 생성 할 수 있습니다.
Gymbo의 또 다른 독특한 특징은 확률 적 기호 변수를 추적 할 수 있다는 것입니다. 우리는 [3] 에 제안 된 PBRANC 알고리즘을 채택하고 현재 개별 균일, Bernoulli 및 이항 분포를 지원합니다.
Gymbo는 현재 개발 중이며 버그가있을 수 있습니다. 귀하의 의견과 기여는 항상 대단히 감사합니다.
git clone https://github.com/Koukyosyumei/Gymbo.git
./script/build.sh예제 디렉토리에서 몇 가지 예를 확인하십시오.
Gymbo는 현재 다음 BNF 문법으로 C와 같은 프로그램을 지원합니다.
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 ")"
Hymbo는 현재 경로 제약을 해결할 때 무시
/무시합니다.
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 Command는 다음 명령 줄 옵션을 수락합니다.
-d : 상징적 실행을 위해 최대 깊이를 설정하십시오 (기본값 : 256).-v : Verbosity 레벨을 설정하십시오 (기본값 : 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 : 헤더 전용 라이브러리Gymbo는 헤더 전용 라이브러리로 구성되어 있으므로 고유 한 상징적 실행 도구를 쉽게 만들 수 있습니다.
# 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 : 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 라이브러리 내에서 일부 도우미 기능을 제공하여 Sklearn 및 Pytorch와 같은 유명한 Python 라이브러리의 ML 모델을 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 ) Gymbo는 전적으로 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
