nathan-luevano/silica모든 43억 개의 AArch64 명령어 인코딩에 대한 철저한 차등 검증.
AArch64 디코더가 아키텍처와 불일치하는 지점에 대한 완전한 지도.
Silica는 가능한 모든 4,294,967,296개의 A64 명령어 워드를 순회하며, Capstone, LLVM, Unicorn을 Arm의 기계 판독 가능 명세와 비교하고, 그 차이를 재현 가능한 증거로 전환합니다.
디스어셈블러가 "유효함"이라고 말하는 것은 쉽습니다. 그것이 올바른지 아는 것은 더 어렵습니다. 대부분의 차분 테스트는 도구들이 서로 불일치한다는 것을 밝힐 수 있지만, 독립적인 오라클 없이는 올바른 답을 식별할 수 없습니다. Silica는 Arm의 XML 릴리스를 그 오라클로 사용합니다.
A64는 유난히 철저한 실험을 가능하게 합니다. 명령어는 정확히 32비트 폭이므로 전체 인코딩 공간이 유한하고 열거하는 것이 실용적입니다. Silica는 이 특성을 활용합니다. 아래의 유효성 결과는 추정치나 퍼징 캠페인이 아니며, 가능한 모든 워드가 검사되었습니다.
이 결과는 ISA_A64_xml_A_profile-2026-06_mc (Armv9.6-A)를 사용합니다. 스윕은
전체 2³² 인코딩을 포괄하는 256개의 독립적으로 검증된 샤드로 분할되었습니다.
| 결과 | 개수 | 전체 공간 대비 비율 |
|---|---|---|
| Arm 명세에 의해 할당됨 | 1,799,435,776 | 41.9% |
| Arm 명세에 의해 할당되지 않음 | 2,495,531,520 | 58.1% |
| 발견된 유효성 불일치 | 723,801,678 | 16.9% |
| 최소 업스트림 준비 재현기 | 10 | — |
인코딩이 유효한지에 대한 명세와의 일치도:
| 디코더 | 일치도 | 시각화 |
|---|---|---|
| Capstone | 84.8% | █████████████████████████░░░░░ |
| LLVM | 87.6% | ██████████████████████████░░░░ |
| Unicorn | 88.3% | ██████████████████████████░░░░ |
큰 유효성 격차에는 식별 가능한 원인이 있습니다. Unicorn은 명령어를 실행하고
트랩을 관찰하여 유효성을 테스트하는 반면, 다른 오라클들은 실행 없이 디코딩합니다.
소수의 영역은 컴파일된 명세 오라클이 평가하지 않는 디코드 시점의 UNDEFINED
조건의 영향을 받기도 합니다. Silica는 이러한 한계를 결과에서 매끄럽게 제거하는 대신
기록합니다.
렌더링된 니모닉과 피연산자를 비교하는 것은 유효성 비트를 기록하는 것보다 훨씬 비용이 많이 듭니다. 따라서 Silica는 네 오라클 모두 인코딩을 유효하다고 간주하는 1,266,064,016개의 후보에서 추출한 1,000,000개 워드의 결정적 샘플에 대해 텍스트를 평가합니다. 이는 샘플링된 결과이며, 철저한 유효성 수치와는 의도적으로 분리되어 유지됩니다.
| 샘플 내 분류 | 레코드 | 비율 |
|---|---|---|
| 피연산자 렌더링 차이 | 862,648 | 86.3% |
| 정규화 검토 필요 | 137,352 | 13.7% |
이 샘플은 정규화 및 표현 작업을 찾아내는 데 유용하며, 모든 텍스트 렌더링에 대한 철저한 포괄을 주장하지 않습니다.
스윕 엔진은 대규모 연구 데이터셋을 생성합니다. **silica-scope**는 그 데이터셋을 접근하기 쉽게 만들어 주는 동반 터미널 앱입니다. 완성된 Silica 아티팩트 디렉터리를 열고 주요 지표를 탐색하고, 256개 샤드 인코딩 맵을 검사하고, 불일치를 필터링하고, 임의의 32비트 워드를 조회하고, 제출 준비가 된 재현기를 읽을 수 있게 해줍니다.
Python 3.11 이상과 함께 PyPI에서 설치하세요:
pipx install silica-scope
그런 다음 Silica 체크아웃에서 실행하거나 아티팩트 디렉터리를 지정하세요:
silica-scope
silica-scope /path/to/silica/artifacts
silica-scope --report
silica-scope는 네이티브 디코더 의존성이 없는 순수 Python 리더입니다. 철저한
스윕을 실행하지 않으며, 저장소의 더 작은 공개 아티팩트 세트를 우아하게 처리합니다.
패널, 키보드 컨트롤, 아티팩트 검색 옵션은 터미널 리더 가이드를
참조하세요.
flowchart LR
XML["Arm XML specification"] --> SPEC["compiled spec oracle"]
SPEC --> SWEEP["parallel 32-bit sweep"]
CAP["Capstone"] --> SWEEP
LLVM["LLVM"] --> SWEEP
UNI["Unicorn"] --> SWEEP
SWEEP --> MAP["validity bitmaps"]
MAP --> DIFF["exhaustive XOR comparison"]
DIFF --> CORPUS["classified disagreement corpus"]
CORPUS --> OUT["metrics · reproducers · result hash"]대용량 경로는 Rust로 작성되었으며 각 디코더를 프로세스 내에서 호출합니다. 오라클당 인코딩당 1비트를 저장하여 철저한 비교를 간결하게 유지하고 불일치를 직접적인 비트맵 연산으로 만듭니다. 크래시는 정확한 명령어 워드까지 이분됩니다.
Python은 명세 컴파일, 정규화, 보고, 독립 검증 계층을 담당합니다. 아티팩트 스키마, 샘플링 규칙, 알려진 한계는 docs/formats.md에 문서화되어 있습니다.
고정된 환경을 만들고 필요한 로컬 입력이 사용 가능한지 확인하세요:
micromamba create -y -p ./.venv -f environment.yml
micromamba run -p ./.venv silica doctor
Arm의 XML 명세는 라이선스 때문에 벤더링되지 않습니다. silica doctor는
Silica가 그것을 어디에서 찾을 것으로 예상하는지와 기타 누락된 전제 조건을
보고합니다.
준비된 체크아웃에서 전체 파이프라인을 실행하려면:
make all
이것은 빠른 스모크 테스트가 아닌 전체 2³² 스윕입니다. 컴파일된 오라클, 샤드 레코드, 유효성 비트맵, 불일치 코퍼스, 공개 지표, 재현기, 안정적인 SHA-256 결과 해시를 생성합니다.
일곱 개의 독립 검증기가 원시 아티팩트로부터 프로젝트의 주장을 재계산합니다. 그들은 생성된 요약을 신뢰하지 않으며, 각 검증기는 자신이 방어하는 결함을 탐지함을 증명하는 픽스처를 가지고 있습니다. 건너뛰거나 잠정적인 상태는 없습니다.
micromamba run -p ./.venv silica verify
고정된 디코더 버전과 새로 재계산된 결과 해시는 별도의 실행을 비교 가능하게 만듭니다. 검증 목표와 현재 상태는 GOALS.yml에 기록되어 있습니다.
Silica는 현재 기본 A64 및 Advanced SIMD 디코딩을 다룹니다. SVE, SVE2, SME, A32/T32, RISC-V, 어셈블러 왕복, 일반 실행 테스트는 v1 연구 범위 밖입니다.
가장 가까운 영감은 x86의 가변 길이 명령어 공간을 탐구하는 Sandsifter입니다. Silica는 고정 폭 인코딩과 독립적인 명세가 완전하고 판정된 비교를 가능하게 하는 AArch64에 동일한 체계적 회의주의 정신을 적용합니다.
Apache 2.0 — LICENSE 참조