Modular Verification of SPARCv8 Code

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...

Full description

Saved in:
Bibliographic Details
Published in:Journal of computer science and technology 2020-11, Vol.35 (6), p.1382-1405
Main Authors: Zha, Jun-Peng, Feng, Xin-Yu, Qiao, Lei
Format: Article
Language:English
Subjects:
Artificial Intelligence
Assembly
Computer Science
Data Structures and Information Theory
Information Systems Applications (incl.Internet)
Logic
Microprocessors
Reasoning
Regular Paper
Safety
Semantics
Software
Software Engineering
Theory of Computation
Verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1000-9000
1860-4749
DOI:10.1007/s11390-020-0536-9