ASMC는 Ghidra의 어셈블리 의미를 CBMC에 연결해 기계어 코드의 속성을 검사하는 도구다. 제작자는 이를 통해 어셈블리의 안전성·ABI 준수 여부와 C 코드와의 동작 일치 여부를 확인할 수 있다고 소개한다.
ASMC 저장소는 컴파일된 ELF 파일을 Ghidra의 p-code 의미에 따라 CBMC의 GOTO IR 형식인 .gb 파일로 변환하는 asmc-lift와, 변환 및 CBMC 실행을 맡는 드라이버 asmc로 구성된다. p-code 의미는 Trail of Bits가 패키징한 sleigh를 사용한다. 기반 도구인 CBMC는 C 프로그램의 제한 모델 검사기다.
함수와 사후 조건을 지정하면 반환 레지스터 값 등을 확인할 수 있고, 잘못된 조건에서는 반례를 출력한다. 예를 들어 42를 반환하는 함수에 43을 기대하는 조건을 주면 검사에 실패한다. 스택의 반환 주소를 덮어쓰거나 호출자 보존 레지스터 R12를 복원하지 않는 경우에도 ABI 위반을 찾아낸다. 사용자 정의 C 하네스를 작성하면 어셈블리 구현의 결과를 원래 C 함수와 비교하는 번역 검증도 할 수 있다.
제작자는 활용 사례로 독립적인 어셈블리 검증, 번역 검증, 외부 어셈블리 연결, 어셈블리용 C 명세, DWARF 디버그 데이터 검증, 패치된 어셈블리 검증, 디컴파일 결과 검증을 들었다. 현재 x86-64 SysV와 RV32/64를 지원하며, Ghidra가 지원하는 다른 아키텍처를 추가하려면 C로 ABI 연결 코드를 작성해야 한다고 설명한다.
한계도 있다. Ghidra p-code에는 지원하지 않는 명령어·플래그와 모델링되지 않은 동작이 있을 수 있고, CBMC에 연결하기 위해 어셈블리 동작을 C로 표현하는 과정에도 타협이 들어간다. 제작자는 이 도구가 정의되지 않은 동작을 찾아내는 데 초점을 둔 엄밀한 C 의미론은 아니라고 밝혔다. asmc-lift는 약 1,000줄의 C++ 코드로 작성됐으며, 제작자는 AI가 자신의 메모와 지시를 바탕으로 도구 제작에 크게 기여했다고 설명했다.
ASMC와 비슷한 접근을 다룬 pcode2c 저장소, Ghidra와 CBMC를 이용한 번역 검증, DWARF 검증 자료도 소개됐다. Z3를 이용한 심볼릭 실행 관련 자료는 refine_assembly, asm_verify4, asm_verify3, asm_verify2, assembly_verify에서 확인할 수 있다. 제작자는 이 작업이 CBAT의 후속 흐름에 있다고 설명하며, Ghidra p-code가 Mario 에뮬레이션에 충분한 사례도 언급했다.
부록: 원문 예시
Output: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x assemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/assemble.log ELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/target.elf Harness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/demo.c (x86-64 SysV) Checking: safety and scalar ABI obligations only (no --post). seed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/seed.log lift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/lift.log ASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008) link: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/link.log cbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/cbmc.log [asmc_target.asmc.13] line 6 unexpected return address (possible clobbered stack return address or incorrect RSP); 0x401007 pcode[2] RET (RETURN) Machine: 0x401007 pcode[2] RET (RETURN) Counterexample (harness/reference values; use --full-trace for all values and machine steps): Trace for asmc_target.asmc.13: demo.c:94 inreg.rax=0ul demo.c:95 inreg.rcx=0ul demo.c:96 inreg.rdx=0ul demo.c:97 inreg.rbx=0ul demo.c:98 inreg.rsp=4344ul demo.c:99 inreg.rbp=0ul demo.c:100 inreg.rsi=0ul demo.c:101 inreg.rdi=0ul demo.c:102 inreg.r8=0ul demo.c:103 inreg.r9=0ul demo.c:104 inreg.r10=0ul demo.c:105 inreg.r11=0ul demo.c:106 inreg.r12=0ul demo.c:107 inreg.r13=0ul demo.c:108 inreg.r14=0ul demo.c:109 inreg.r15=0ul demo.c:110 inreg.cf=0 demo.c:111 inreg.pf=0 demo.c:112 inreg.af=0 demo.c:113 inreg.zf=0 demo.c:114 inreg.sf=0 demo.c:115 inreg.of=0 demo.c:116 inreg.df=0 Recent machine instructions: 0x401000 MOV dword ptr [RSP],0x2a 0x401007 RET Violated property: file /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/lifted.gb.asm function asmc_target line 6 thread 0 unexpected return address (possible clobbered stack return address or incorrect RSP); 0x401007 pcode[2] RET (RETURN) asmc_tmp_12 == asmc_tmp_13 Return destination: 0x7fff0000002a (140733193388074) Expected harness return sentinel: 0x7fffffff0000 Trace and details: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-8j5vcj4x/cbmc.log FAIL: counterexample found
Output: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp assemble: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/assemble.log ELF: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/target.elf Harness: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/demo.c (x86-64 SysV) Checking: safety and scalar ABI obligations only (no --post). seed: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/seed.log lift: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/lift.log ASMC lift range: myfun has no ELF size; reachable code window in .text [0x401000, 0x401008) link: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/link.log cbmc: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/cbmc.log [asmc_sysv_check.assertion.5] line 91 ABI violation: callee-saved register R12 was not restored Counterexample (harness/reference values; use --full-trace for all values and machine steps): Trace for asmc_sysv_check.assertion.5: demo.c:94 inreg.rax=0ul demo.c:95 inreg.rcx=0ul demo.c:96 inreg.rdx=0ul demo.c:97 inreg.rbx=0ul demo.c:98 inreg.rsp=4344ul demo.c:99 inreg.rbp=0ul demo.c:100 inreg.rsi=0ul demo.c:101 inreg.rdi=0ul demo.c:102 inreg.r8=0ul demo.c:103 inreg.r9=0ul demo.c:104 inreg.r10=0ul demo.c:105 inreg.r11=0ul demo.c:106 inreg.r12=16777216ul demo.c:107 inreg.r13=0ul demo.c:108 inreg.r14=0ul demo.c:109 inreg.r15=0ul demo.c:110 inreg.cf=0 demo.c:111 inreg.pf=0 demo.c:112 inreg.af=0 demo.c:113 inreg.zf=0 demo.c:114 inreg.sf=0 demo.c:115 inreg.of=0 demo.c:116 inreg.df=0 Recent machine instructions: 0x401000 MOV R12,0x2a 0x401007 RET Violated property: file /home/philip/vibe_coding/asmc/include/asmc_x86.h function asmc_sysv_check line 91 thread 0 ABI violation: callee-saved register R12 was not restored return_value_asmc_get_reg$3 == frame->preserved[(signed long int)2] Trace and details: /home/philip/philzook58.github.io/_drafts/asmc-out/myfun-0_l28dvp/cbmc.log FAIL: counterexample found
댓글 (0)
로그인하면 이 기사에 내 생각을 남길 수 있어요