NDLI: Certified self-modifying code

Content Provider	ACM Digital Library
Author	Shao, Zhong Vaynberg, Alexander Cai, Hongxu
Abstract	Self-modifying code (SMC), in this paper, broadly refers to anyprogram that loads, generates, or mutates code at runtime. It is widely used in many of the world's critical software systems tosupport runtime code generation and optimization, dynamic loading and linking, OS boot loader, just-in-time compilation, binary translation,or dynamic code encryption and obfuscation. Unfortunately, SMC is alsoextremely difficult to reason about: existing formal verification techniques-including Hoare logic and type system-consistentlyassume that program code stored in memory is fixedand immutable; this severely limits their applicability and power. This paper presents a simple but novel Hoare-logic-like framework that supports modular verification of general von-Neumann machine code with runtime code manipulation. By dropping the assumption that code memory is fixed and immutable, we are forced to apply local reasoningand separation logic at the very beginning, and treat program code uniformly as regular data structure. We address the interaction between separation and code memory and show how to establish the frame rules for local reasoning even in the presence of SMC. Our frameworkis realistic, but designed to be highly generic, so that it can support assembly code under all modern CPUs (including both x86 andMIPS). Our system is expressive and fully mechanized. We prove itssoundness in the Coq proof assistant and demonstrate its power by certifying a series of realistic examples and applications-all of which can directly run on the SPIM simulator or any stock x86 hardware.
Starting Page	66
Ending Page	77
Page Count	12
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/1273442.1250743
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	42
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	Runtime code manipulation Modular verification Self-modifying code Assembly code verification Hoare logic
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

Certified self-modifying code

Certified assembly programming with embedded code pointers

Sound Modular Verification of C Code Executing in an Unverified Context

Certified self-modifying code (2007)

Certified Self-Modifying Code (2007)

Modular verification of assembly code with stack-based control abstractions

Frame rules from answer types for code pointers

Cartesian hoare logic for verifying k-safety properties

Functional programming is not self-modifying code

Certified self-modifying code

Similar Documents

Certified self-modifying code

Certified assembly programming with embedded code pointers

Sound Modular Verification of C Code Executing in an Unverified Context

Certified self-modifying code (2007)

Certified Self-Modifying Code (2007)

Modular verification of assembly code with stack-based control abstractions

Frame rules from answer types for code pointers

Cartesian hoare logic for verifying k-safety properties

Functional programming is not self-modifying code

Certified self-modifying code