Modular Verification of SPARCv8 Code
- PDF / 953,841 Bytes
- 24 Pages / 595 x 842 pts (A4) Page_size
- 90 Downloads / 186 Views
Modular Verification of SPARCv8 Code Jun-Peng Zha1,2 , Xin-Yu Feng1,2,∗ , Member, CCF, ACM, and Lei Qiao3 , Member, CCF 1
Department of Computer Science and Technology, Nanjing University, Nanjing 210023, China
2
State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210023, China
3
Beijing Institute of Control Engineering, Beijing 100080, China
E-mail: [email protected]; [email protected]; [email protected] Received April 11, 2020; revised October 24, 2020. Abstract Inline assembly code is common in system software to interact with the underlying hardware platforms. The safety and correctness of the assembly code is crucial to guarantee the safety of the whole system. In this paper, we propose a practical Hoare-style program logic for verifying SPARC (Scalable Processor Architecture) assembly code. The logic supports modular reasoning about the main features of SPARCv8 ISA (instruction set architecture), including delayed control transfers, delayed writes to special registers, and register windows. It also supports relational reasoning for refinement verification. We have applied it to verify that there is a contextual refinement between a context switch routine in SPARCv8 and a switch primitive. The program logic and its soundness proof have been mechanized in Coq. Keywords Scalable Processor Architecture Version 8 (SPARCv8), assembly code verification, context switch, Coq, refinement verification
1
Introduction
Operating system kernels are at the most foundational layer of computer software systems. To interact directly with hardware, many important components in OS kernels are implemented in assembly, such as the context switch code or the code that manages interrupts. In addition, there is also code written directly in assembly to achieve high performance (e.g., memcpy in 1 linux v2.6.17.10○ ). Correctness of such assembly code is crucial to ensure the safety and security of the whole system. However, assembly code verification remains a challenging task in existing work on OS kernel verification (e.g., [1–3]), where the assembly code is either unverified or verified based on operational semantics without a general program logic. SPARC (Scalable Processor Architecture) is a CPU instruction set architecture (ISA) with high-
2 performance and great flexibility○ . It has been widely used in various processors for workstations and embedded systems. SPARCv8 ISA has some interesting features, which make it a non-trivial task to design a Hoare-style program logic for assembly code. • Delayed Control Transfers. SPARCv8 has two program counters pc and npc. The npc register points to the next instruction to run. Control-transfer instructions in SPARCv8 change npc instead of pc to the target program point, while pc takes the original value of npc. This makes the control transfer happen one cycle later than the execution of the control transfer instructions. • Delayed Writes. The wr instruction that writes a special class of registers such as the window invalid mask register wim doe
Data Loading...
