NDLI: Modular verification of assembly code with stack-based control abstractions

Content Provider	ACM Digital Library
Author	Shao, Zhong Vaynberg, Alexander Feng, Xinyu Ni, Zhaozhong Xiang, Sen
Abstract	Runtime stacks are critical components of any modern software--they are used to implement powerful control structures such as function call/return, stack cutting and unwinding, coroutines, and thread context switch. Stack operations, however, are very hard to reason about: there are no known formal specifications for certifying C-style setjmp/longjmp, stack cutting and unwinding, or weak continuations (in C--). In many proof-carrying code (PCC) systems, return code pointers and exception handlers are treated as general first-class functions (as in continuation-passing style) even though both should have more limited scopes.In this paper we show that stack-based control abstractions follow a much simpler pattern than general first-class code pointers. We present a simple but flexible Hoare-style framework for modular verification of assembly code with all kinds of stackbased control abstractions, including function call/return, tail call, setjmp/longjmp, weak continuation, stack cutting, stack unwinding, multi-return function call, coroutines, and thread context switch. Instead of presenting a specific logic for each control structure, we develop all reasoning systems as instances of a generic framework. This allows program modules and their proofs developed in different PCC systems to be linked together. Our system is fully mechanized. We give the complete soundness proof and a full verification of several examples in the Coq proof assistant.
Starting Page	401
Ending Page	414
Page Count	14
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/1133255.1134028
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	41
Issue Number	6
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Stack-based Proof-carrying code Modularity Assembly code verification Control abstractions
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Modular verification of assembly code with stack-based control abstractions

Modular verification of concurrent assembly code with dynamic thread creation and termination

Toward a foundational typed assembly language

Modular development of certified program verifiers with a proof assistant

Certified self-modifying code

Certified assembly programming with embedded code pointers

Modular verification of preemptive OS kernels

A general framework for certifying garbage collectors and their mutators

A provably sound TAL for back-end optimization

Modular verification of assembly code with stack-based control abstractions

Similar Documents

Modular verification of assembly code with stack-based control abstractions

Modular verification of concurrent assembly code with dynamic thread creation and termination

Toward a foundational typed assembly language

Modular development of certified program verifiers with a proof assistant

Certified self-modifying code

Certified assembly programming with embedded code pointers

Modular verification of preemptive OS kernels

A general framework for certifying garbage collectors and their mutators

A provably sound TAL for back-end optimization

Modular verification of assembly code with stack-based control abstractions