Automatic Generation and Validation of Instruction Encoders and Decoders
A
u
t
o
m
a
t
i
c
G
e
n
e
r
a
t
i
o
n
a
n
d
V
a
l
i
d
a
t
i
o
n
o
f
I
n
s
t
r
u
c
t
i
o
n
E
n
c
o
d
e
r
s
a
n
d
D
e
c
o
d
e
r
s
Xiangzhe Xu, Jinhua Wu,
Yuting Wang
, Zhenguo Yin, Pengfei Li
Shanghai Jiao Tong University, Shanghai, China
Computer Aided Verification (CAV) 2021
M
o
t
i
v
a
t
i
o
n
•
B
a
c
k
g
r
o
u
n
d
:
M
a
n
i
p
u
l
a
t
i
o
n
o
f
M
a
c
h
i
n
e
C
o
d
e
•
P
r
o
b
l
e
m
:
M
u
t
u
a
l
I
n
v
e
r
s
i
o
n
b
e
t
w
e
e
n
E
n
c
o
d
i
n
g
a
n
d
D
e
c
o
d
i
n
g
2
Add EAX, EBX
001001010…
Compilers & Assemblers
Binary Analysis Tools
…
A
b
s
t
r
a
c
t
I
n
s
t
r
u
c
t
i
o
n
s
M
a
c
h
i
n
e
I
n
s
t
r
u
c
t
i
o
n
s
Machine Code
C
h
a
l
l
e
n
g
e
s
•
V
a
r
i
e
t
y
a
n
d
C
o
m
p
l
e
x
i
t
y
o
f
I
n
s
t
r
u
c
t
i
o
n
F
o
r
m
a
t
s
•
E
x
a
m
p
l
e
:
3
2
-
b
i
t
X
8
6
I
n
s
t
r
u
c
t
i
o
n
F
o
r
m
a
t
3
T
o
k
e
n
s
:
F
i
e
l
d
s
:
P
r
e
v
i
o
u
s
W
o
r
k
•
F
o
r
m
a
l
i
z
a
t
i
o
n
o
f
I
n
s
t
r
u
c
t
i
o
n
S
y
n
t
a
x
(
N
o
t
S
e
m
a
n
t
i
c
s
)
•
Summary of Representative Work:
4
C
o
n
t
r
i
b
u
t
i
o
n
•
A
N
o
v
e
l
F
r
a
m
e
w
o
r
k
f
o
r
F
o
r
m
a
l
i
z
i
n
g
I
n
s
t
r
u
c
t
i
o
n
F
o
r
m
a
t
s
t
h
a
t
S
u
p
p
o
r
t
s
A
u
t
o
m
a
t
i
c
V
e
r
i
f
i
c
a
t
i
o
n
o
f
M
u
t
u
a
l
I
n
v
e
r
s
i
o
n
5
C
o
n
t
r
i
b
u
t
i
o
n
•
A
N
o
v
e
l
F
r
a
m
e
w
o
r
k
f
o
r
F
o
r
m
a
l
i
z
i
n
g
I
n
s
t
r
u
c
t
i
o
n
F
o
r
m
a
t
s
t
h
a
t
S
u
p
p
o
r
t
s
A
u
t
o
m
a
t
i
c
V
e
r
i
f
i
c
a
t
i
o
n
o
f
M
u
t
u
a
l
I
n
v
e
r
s
i
o
n
6
T
h
e
F
r
a
m
e
w
o
r
k
•
C
S
L
E
D
S
p
e
c
i
f
i
c
a
t
i
o
n
L
a
n
g
u
a
g
e
•
Patterns Describing Instruction Structures
•
Unambiguous Relations Between Abstract
and Binary Instructions
•
G
e
n
e
r
a
t
i
o
n
o
f
E
n
c
o
d
e
r
s
a
n
d
D
e
c
o
d
e
r
s
•
Generating Definitions in Coq
•
V
a
l
i
d
a
t
i
o
n
o
f
M
u
t
u
a
l
I
n
v
e
r
s
i
o
n
•
Synthesizing Proofs in Coq
•
Resolve Verification Conditions
in SMT Solvers
7
Instruction
Formats
E
n
c
o
d
e
Instruction
Specifications
Algorithms
Encoder
Decoder
Proofs of Mutual
Inversion
I
n
p
u
t
O
n
P
a
p
e
r
I
n
C
S
L
E
D
I
n
C
+
+
I
n
C
o
q
E
v
a
l
u
a
t
i
o
n
&
C
o
n
c
l
u
s
i
o
n
•
I
m
p
l
e
m
e
n
t
a
t
i
o
n
•
Algorithms: 5.2k lines of C++
•
Coq Library: 1k lines of Coq (version 8.11.0)
•
SMT Solver: Z3 with Theory of Bit-Vectors
•
T
e
s
t
C
a
s
e
:
1
8
6
R
e
p
r
e
s
e
n
t
a
t
i
v
e
X
8
6
-
3
2
I
n
s
t
r
u
c
t
i
o
n
s
•
Sufficient for Assembling All X86-32 Instructions in CompCert
•
260 Lines of Specifications in CSLED
•
Generates 45k Definitions and 42k Proofs in Coq
•
A
r
t
i
f
a
c
t
a
v
a
i
l
a
b
l
e
a
t
:
•
https://zenodo.org/record/4720184#.YNBOZGgzZPY
8
K
e
y
I
d
e
a
s
•
Classes
•
Abstract Syntax as Inductive Types
•
Patterns
for Relating Abstract and
Binary Instructions
•
Nested Classes
•
Well-formedness Conditions
•
Determinacy of Decoding
•
Non-overlapping of Encoding
•
…
•
Proofs of Mutual Inversion
9
Coq Proofs
Patterns
SMT
Checking
Well-
formedness
E
v
a
l
u
a
t
i
o
n
•
I
m
p
l
e
m
e
n
t
a
t
i
o
n
•
Algorithms: 5.2k lines of C++
•
Coq Library: 1k lines of Coq (version 8.11.0)
•
T
e
s
t
C
a
s
e
:
1
8
6
R
e
p
r
e
s
e
n
t
a
t
i
v
e
X
8
6
-
3
2
I
n
s
t
r
u
c
t
i
o
n
s
•
Operands with Most Complex Dependency (e.g., Addressing Modes)
•
Sufficient for Assembling All X86-32 Instructions in CompCert
•
260 Lines of Specifications in CSLED
10
C
o
n
c
l
u
s
i
o
n
•
We introduced a framework for
•
Developing Unambiguous Formalization of Instruction Formats
•
Automatically Generating Instruction Encoders and Decoders
•
Automatically Verifying the Mutual Inversion of Encoding and Decoding
•
Artifact available at:
•
https://zenodo.org/record/4720184#.YNBOZGgzZPY
•
F
u
t
u
r
e
W
o
r
k
:
•
Developing a formal theory for the specification language
•
Applications to full X86 and other instruction sets (e.g., RSIC-V, ARM)
•
Formalization of binary analysis and manipulation
11
Hello everyone, this is Yuting Wang from Shanghai Jiao Tong University.
Today I will discuss the automatic generation of verified encoders and decoders for machine instructions.
This is a joint work with Xiangzhe Xu, Jinhua Wu, Zhenguo Yin and Pengfei Li.
This study presents a novel framework for formalizing instruction formats to support automatic verification of mutual inversion frameworks. It addresses challenges posed by the variety and complexity of instruction formats, focusing on 32-bit X86 format and providing a detailed exploration of the framework's contributions, design, and evaluation. The proposed framework leverages CSLED specification language, patterns for describing instruction structures, and algorithms for validation and synthesis of proofs, emphasizing the generation of encoders and decoders. The implementation includes over 5.2k lines of C++ code and 1k lines of Coq library, contributing significantly to the field of automatic generation and validation of instruction encoders and decoders.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Automatic Generation and Validation of Instruction Encoders and Decoders Xiangzhe Xu, Jinhua Wu, Yuting Wang, Zhenguo Yin, Pengfei Li Shanghai Jiao Tong University, Shanghai, China Computer Aided Verification (CAV) 2021
Motivation Background: Manipulation of Machine Code Machine Instructions Abstract Instructions Compilers & Assemblers ?????? Machine Code Add EAX, EBX 001001010 ?????? Binary Analysis Tools Problem: Mutual Inversion between Encoding and Decoding ? ?,?????? ? = ? ?????? ? = ? 2
Challenges Variety and Complexity of Instruction Formats Example: 32-bit X86 Instruction Format 1 byte ModRM ModRM 1 byte Opcode Opcode Opcode 1 byte SIB 4 byte 4 byte Tokens: 0x03 ModRM 0x1C 0x18 Opcode 0x90 0x03 SIB 0x8C Immediate Displacement NOP NOP Fields: Mod 00 00 RegOp 011 011 RM 100 000 Scale 10 Index 001 Base 100 EBX , [4 ADD ADD EBX EBX , , [4 * * ECX , ADD ADD EBX ESP] ESP] [ [EAX EAX] ] ECX + + 3
Contribution A Novel Framework for Formalizing Instruction Formats that Supports Automatic Verification of Mutual Inversion FrameworksSupport MutualInversion Automation Formalization Instr. Fmt. SLED YES YES NO NO RockSalt YES YES YES NO Narcissus NO YES YES NO Our Framework YES YES YES YES 6
The Framework Instruction Formats CSLED Specification Language Patterns Describing Instruction Structures Unambiguous Relations Between Abstract and Binary Instructions On Paper Encode Instruction Specifications In CSLED Input Generation of Encoders and Decoders Generating Definitions in Coq Algorithms In C++ Validation of Mutual Inversion Synthesizing Proofs in Coq Resolve Verification Conditions in SMT Solvers Proofs of Mutual Inversion In Coq Encoder Decoder 7
Evaluation & Conclusion Implementation Algorithms: 5.2k lines of C++ Coq Library: 1k lines of Coq (version 8.11.0) SMT Solver: Z3 with Theory of Bit-Vectors Test Case: 186 Representative X86-32 Instructions Sufficient for Assembling All X86-32 Instructions in CompCert 260 Lines of Specifications in CSLED Generates 45k Definitions and 42k Proofs in Coq Artifact available at: https://zenodo.org/record/4720184#.YNBOZGgzZPY 8
