Machine instruction syntax and semantics in higher order logic

Neophytos G. Michael, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

17 Scopus citations

Abstract

Proof-carrying code and other applications in computer security require machine-checkable proofs of properties of machine-language programs. These in turn require axioms about the opcode/operand encoding of machine instructions and the semantics of the encoded instructions. We show how to specify instruction encodings and semantics in higher-order logic, in a way that preserves the factoring of similar instructions in real machine architectures. We show how to automatically generate proofs of instruction decodings, global invariants from local invariants, Floyd-Hoare rules and predicate transformers, all from the specification of the instruction semantics. Our work is implemented in ML and Twelf, and all the theorems are checked in Twelf.

Original languageEnglish (US)
Title of host publicationAutomated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings
EditorsDavid McAllester
PublisherSpringer Verlag
Pages7-24
Number of pages18
ISBN (Electronic)3540676643, 9783540676645
DOIs
StatePublished - Jan 1 2000
Event17th International Conference on Automated Deduction, CADE 2000 - Pittsburgh, United States
Duration: Jun 17 2000Jun 20 2000

Publication series

NameLecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)
Volume1831
ISSN (Print)0302-9743

Other

Other17th International Conference on Automated Deduction, CADE 2000
CountryUnited States
CityPittsburgh
Period6/17/006/20/00

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Machine instruction syntax and semantics in higher order logic'. Together they form a unique fingerprint.

  • Cite this

    Michael, N. G., & Appel, A. W. (2000). Machine instruction syntax and semantics in higher order logic. In D. McAllester (Ed.), Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings (pp. 7-24). (Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science); Vol. 1831). Springer Verlag. https://doi.org/10.1007/10721959_2