Journal of Computer Science and Technology ›› 2020, Vol. 35 ›› Issue (6): 1382-1405.doi: 10.1007/s11390-020-0536-9

Special Issue: Software Systems

Previous Articles     Next Articles

Modular Verification of SPARCv8 Code

Jun-Peng Zha1,2, Xin-Yu Feng1,2,*, Member, CCF, ACM, and Lei Qiao3, Member, CCF        

  1. 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
  • Received:2020-04-11 Revised:2020-10-24 Online:2020-11-20 Published:2020-12-01
  • Contact: Xin-Yu Feng E-mail:xyfeng@nju.edu.cn
  • About author:Jun-Peng Zha is a Ph.D. candidate in the Department of Computer Science and Technology at Nanjing University, Nanjing. He received his M.S. degree in computer science from the University of Science and Technology of China, Hefei, in 2019, and his B.S. degree in software engineering from Shandong University at Weihai in 2016. His research interests are in programming languages and formal methods, with focus on the verification of compiler and low-level assembly code.
  • Supported by:
    This work was supported by the National Natural Science Foundation of China under Grant No. 61632005.

PDF (PC)

34

Supplement

1

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.

Key words: Scalable Processor Architecture Version 8 (SPARCv8); assembly code verification; context switch; Coq; refinement verification;

[1] Xu F, Fu M, Feng X, Zhang X, Zhang H, Li Z. A practical verification framework for preemptive OS kernels. In Proc. the 28th International Conference, July 2016, pp.59-79.
[2] Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S. seL4:Formal verification of an OS Kernel. In Proc. the 22nd ACM Symposium on Operating Systems Principles, Oct. 2009, pp.207-220.
[3] Gu R, Koenig J, Ramananandro T, Shao Z, Wu X N, Weng S C, Zhang H, Guo Y. Deep specifications and certified abstraction layers. In Proc. the 42nd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Jan. 2015, pp.59-5608.
[4] Zha J, Feng X, Qiao L. Modular verification of SPARCv8 code. In Proc. the 16th Asian Symposium on Programming Languages and Systems, December 2018, pp.245-263.
[5] Feng X, Shao Z, Vaynberg A, Xiang S, Ni Z. Modular verification of assembly code with stack-based control abstractions. In Proc. the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, June 2006, pp.401-414.
[6] Leroy X, Blazy S. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 2008, 41(1):1-31.
[7] Wang J, Fu M, Qiao L, Feng X. Formalizing SPARCv8 instruction set architecture in Coq. In Proc. the 3rd International Symposium on Dependable Software Engineering:Theories, Tools, and Applications, Oct. 2017, pp.300-316.
[8] Reynolds J. Separation logic:A logic for shared mutable data structures. In Proc. the 17th IEEE Symposium on Logic in Computer Science, July 2002, pp.55-74.
[9] Liang H, Feng X, Shao Z. Compositional verification of termination-preserving refinement of concurrent programs. In Proc. the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, July 2014, Article No. 65.
[10] Necula G C, Lee P. Safe kernel extensions without run-time checking. In Proc. the 2nd USENIX Symp. Operating System Design and Implementation, October 1996, pp.229-243.
[11] Appel A W. Foundational proof-carrying code. In Proc. the 16th Annual IEEE Symposium on Logic in Computer Science, June 1998, pp.247-256.
[12] Morrisett G, Crary K, Glew N, Grossman D, Samuels R, Smith F, Walker D, Weirich S, Zdancewic S. TALx86:A realistic typed assembly language. In Proc. the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, May 1996, pp.25-35.
[13] Morrisett G, Walker D, Crary K, Glew N. From system F to typed assembly language. In Proc. the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan. 1998, pp.85-97.
[14] Yu D, Nadeem A H, Shao Z. Building certified libraries for PCC:Dynamic storage allocation. Science of Computer Programming, 2004, 50(1/2/3):101-127.
[15] Ni Z, Shao Z. Certified assembly programming with embedded code pointers. In Proc. the 33rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, January 2006, pp.320-333.
[16] Tan G, Appel A W. A compositional logic for control flow. In Proc. the 7th International Conference on Verification, Model Checking, and Abstract Interpretation, Jan. 2006, pp.80-94.
[17] Myreen M O, Gordon M J. Hoare logic for realistically modelled machine code. In Proc. the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, March 2007, pp.568-582.
[18] Hou Z, Sanán D, Tiu A, Liu Y, Hoa K C. An executable formalisation of the SPARCv8 instruction set architecture:A case study for the LEON3 processor. In Proc. the 21st International Symposium on Formal Methods, November 2016, pp.388-405.
[19] Ni Z, Yu D, Shao Z. Using XCAP to certify realistic systems code:Machine context management. In Proc. the 20th International Conference on Theorem Proving in Higher Order Logics, Sept. 2007, pp.189-206.
[20] Yang J, Hawblitzel C. Safe to the last instruction:Automated verification of a type-safe operating system. In Proc. the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2010, pp.99-110.
[21] Berdine J, Calcagno C, O'Hearn P W. Symbolic execution with separation logic. In Proc. the 3rd Asian Symposium on Programming Languages and Systems, November 2005, pp.52-68.
[22] Berdine J, Calcagno C, O'Hearn P W. Smallfoot:Modular automatic assertion checking with separation logic. In Proc. the 4th International Symposium on Formal Methods for Components and Objects, November 2005, pp.115-137.
[1] Wen-Jun Shi, Qin-Xiang Cao, Yu-Xin Deng, Han-Ru Jiang, Yuan Feng. Symbolic Reasoning About Quantum Circuits in Coq [J]. Journal of Computer Science and Technology, 2021, 36(6): 1291-1306.
[2] Zhi Ma, Lei Qiao, Meng-Fei Yang, Shao-Feng Li, Jin-Kun Zhang. Verification of Real Time Operating System Exception Management Based on SPARCv8 [J]. Journal of Computer Science and Technology, 2021, 36(6): 1367-1387.
[3] Yu Guo(郭 宇), Xin-Yu Jiang(蒋信予), and Yi-Yun Chen(陈意云). Certification of Thread Context Switching [J]. , 2010, 25(4): 827-840.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] Liu Mingye; Hong Enyu;. Some Covering Problems and Their Solutions in Automatic Logic Synthesis Systems[J]. , 1986, 1(2): 83 -92 .
[2] Wang Xuan; Lü Zhimin; Tang Yuhai; Xiang Yang;. A High Resolution Chinese Character Generator[J]. , 1986, 1(2): 1 -14 .
[3] C.Y.Chung; H.R.Hwa;. A Chinese Information Processing System[J]. , 1986, 1(2): 15 -24 .
[4] Gao Qingshi; Zhang Xiang; Yang Shufan; Chen Shuqing;. Vector Computer 757[J]. , 1986, 1(3): 1 -14 .
[5] Pan Qijing;. A Routing Algorithm with Candidate Shortest Path[J]. , 1986, 1(3): 33 -52 .
[6] Zhang Cui; Zhao Qinping; Xu Jiafu;. Kernel Language KLND[J]. , 1986, 1(3): 65 -79 .
[7] Zhong Renbao; Xing Lin; Ren Zhaoyang;. An Interactive System SDI on Microcomputer[J]. , 1987, 2(1): 64 -71 .
[8] Qiao Xiangzhen;. An Efficient Parallel Algorithm for FFT[J]. , 1987, 2(3): 174 -190 .
[9] Sun Yongqiang; Lu Ruzhan; Huang Xiaorong;. Termination Preserving Problem in the Transformation of Applicative Programs[J]. , 1987, 2(3): 191 -201 .
[10] Huang Guoxiang; Liu Jian;. A Key-Lock Access Control[J]. , 1987, 2(3): 236 -243 .

ISSN 1000-9000(Print)

         1860-4749(Online)
CN 11-2296/TP

 Home
Editorial Board
Author Guidelines
Subscription		 Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
Tel.:86-10-62610746
E-mail: jcst@ict.ac.cn
 
  Copyright ©2015 JCST, All Rights Reserved