ISA specification

[Google Scholar]

Notes: instruction set architecture, ASL, ISPS, L3, LISA, Sail language, SLED, CPU verification, translation validation, weak memory

Specifications of instruction set architectures.

Arm architecture, Arm Architecture Specification Language (ASL), Binary analysis, Binary lifter, BinRec binary lifter, Capstone disassembler, CPU verification, Dagger binary lifter, Instruction set architecture, Instruction Set Processor (ISP), L3 specification language, LISA, LLVM-MCtoLL binary lifter, McSema binary lifter, QEMU, Remill binary lifting library, reopt binary lifter, rev.ng reverse engineering tool, Sail ISA specification language, Specification language for encoding and decoding (SLED), TCG (Tiny Code Generator) intermediate representation, zydis x86 decoder/disassembler library

  • An in-depth analysis of disassembly on full-scale x86/x64 binaries [andriesse:usenix:2016]
  • Detailed models of instruction set architectures: From pseudocode to formal semantics [armstrong:arw:2018]
  • Isla: Integrating full-scale ISA semantics and axiomatic concurrency models [armstrong:cav:2021]
  • ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS [armstrong:popl19:2019]
  • The state of Sail [armstrong:spisa:2019]
  • Automatic generation of peephole superoptimizers [bansal:asplos:2006]
  • Binary translation using peephole superoptimizers [bansal:osdi:2008]
  • ISP: A language to describe instruction sets and other register transfer systems [barbacci:cmu:1972]
  • Instruction set processor specifications (ISPS): The notation and its applications [barbacci:ieee:1981]
  • Specification of Intel IA-32 using an architecture description language [bastian:adl:2005]
  • Verified security for the Morello capability-enhanced prototype Arm architecture [bauereiss:ucam:2021]
  • A high assurance virtualization platform for ARMv8 [baumann:eucnc:2016]
  • The PMS and ISP descriptive systems for computer structures [bell:afips:1970]
  • Computer structures: Readings and examples [bell:book:1971]
  • Putting it all together - Formal verification of the VAMP [beyer:ijsttt:2006]
  • The fallacy of spec-based design [bhatt:sefm:2003]
  • Engineering with logic: Rigorous test-oracle specification and validation for TCP/IP and the sockets API [bishop:jacm:2019]
  • Designing a CPU model: from a pseudo-formal document to fast code [blanqui:rapido:2011]
  • Vale: Verifying high-performance cryptographic assembly code [bond:usenix:2017]
  • BAP: A binary analysis platform [brumley:cav:2011]
  • Formal verification of pipelined Y86-64 microprocessors with UCLID5 [bryant:cmu:2018]
  • Extracting behaviour from an executable instruction set model [campbell:fmcad:2016]
  • Formalization and automatic derivation of code generators [cattell:phd:1978]
  • Automatic derivation of code generators from machine descriptions [cattell:toplas:1980]
  • UQBT: Adaptable binary translation at low cost [cifuentes:computer:2000]
  • Specifying the semantics of machine instructions [cifuentes:iwpc:1998]
  • Reverse interpretation + mutation analysis = automatic retargeting [collberg:pldi:1997]
  • Machine code verification of a tiny ARM hypervisor [dam:ted:2013]
  • Machine code verification of a tiny ARM hypervisor [dam:trusted:2013]
  • A complete formal semantics of x86-64 user-level instruction set architecture [dasgupta:pldi:2019]
  • Scalable validation of binary lifters [dasgupta:pldi:2020]
  • Formal specification of the x86 instruction set architecture [degenbaev:phd:2012]
  • Automatically generating instruction selectors using declarative machine descriptions [dias:popl:2010]
  • A formal description of SYSTEM/360 [falkoff:ibm:1964]
  • Describing instruction set processors using nML [fauth:edtc:1995]
  • Automatic checking of instruction specifications [fernandez:icse:1997]
  • Modelling the ARMv8 architecture, operationally: concurrency and ISA [flur:popl:2016]
  • Mixed-size concurrency: ARM, POWER, C/C++11, and SC [flur:popl:2017]
  • A HOL specification of the ARM instruction set architecture [fox:cambridge:2001]
  • Verified compilation of CakeML to multiple machine-code targets [fox:cpp:2017]
  • A trustworthy monadic formalization of the ARMv7 instruction set architecture [fox:itp:2010]
  • Directions in ISA specification [fox:itp:2012]
  • Improved tool support for machine-code decompilation in HOL4 [fox:itps:2015]
  • Formal specification and verification of ARM6 [fox:tphols:2003]
  • End-to-end formal verification of a RISC-V processor extended with capability pointers [gao:fmcad:2021]
  • Automated synthesis of symbolic instruction encodings from I/O samples [godefroid:pldi:2012]
  • Abstract stobjs and their application to ISA modeling [goel:acl2:2013]
  • Balancing automation and control for formal verification of microprocessors [goel:cav:2021]
  • Verifying x86 instruction implementations [goel:cpp:2020]
  • Simulation and formal verification of x86 machine-code programs that make system calls [goel:fmcad:2014]
  • Engineering a formal, executable x86 ISA simulator for software verification [goel:pcs:2017]
  • Formal verification of application and system programs based on a validated x86 ISA model [goel:phd:2016]
  • Using x86isa for microcode verification [goel:spisa:2019]
  • An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors [gray:micro:2015]
  • A robust machine code proof framework for highly secure applications [hardin:acl2:2006]
  • Lifting assembly to intermediate representation: A novel approach leveraging compilers [hasabnis:asplos:2016]
  • Towards verified binary raising [hendrix:itp:2019]
  • MIPS: A microprocessor architecture [hennessy:micro:1982]
  • Stratified synthesis: Automatically learning the x86-64 instruction set [heule:pldi:2016]
  • Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations [hsiao:micro:2021]
  • Reverse-engineering instruction encodings [hsieh:usenix:2001]
  • Instruction-level abstraction (ILA): A uniform specification for system-on-chip (SoC) verification [huang:todaes:2019]
  • Microprocessor design verification [hunt:jar:1989]
  • High-level separation logic for low-level code [jensen:popl:2013]
  • Examiner: Automatically locating inconsistent instructions between real devices and CPU emulators for Arm [jiang:arxiv:2021]
  • Towards verified faithful simulation [joloboff:dsetta:2015]
  • Towards a formal model of the x86 ISA [kaufmann:utaustin:2012]
  • Coq: The world's best macro assembler? [kennedy:ppdp:2013]
  • Automated formal verification of processors based on architectural models [kuhne:fmcad:2010]
  • Zsim: A fast architectural simulator for ISA design-space exploration [lifshitz:wish:2011]
  • TSL: A system for generating abstract interpreters and its application to machine-code analysis [lim:toplas:2013]
  • Proving LTL properties of bitvector programs and decompiled binaries (extended) [liu:arxiv:2021]
  • Pydgin: generating fast instruction set simulators from simple architecture descriptions with meta-tracing JIT compilers [lockhart:ispass:2015]
  • Processor description languages [mishra:book:2008]
  • RockSalt: Better, faster, stronger SFI for the x86 [morrisett:pldi:2012]
  • Axiomatic hardware-software contracts for security [mosier:isca:2022]
  • Hoare logic for ARM machine code [myreen:fse:2007]
  • A verified runtime for a verified theorem prover [myreen:itp:2011]
  • Verified just-in-time compiler on x86 [myreen:popl:2010]
  • Verified LISP Implementations on ARM, x86 and PowerPC [myreen:tphols:2009]
  • Polymorphic type inference for machine code [noonan:pldi:2016]
  • Design of a symbolically executable embedded hypervisor [nordholz:eurosys:2020]
  • N-version disassembly: Differential testing of x86 disassemblers [paleari:issta:2010]
  • PDP-11/45 processor handbook [pdp11:book:1973]
  • Simplifying ARM concurrency: Multicopy-atomic axiomatic and operational models for ARMv8 [pulte:popl:2017]
  • Machine descriptions to build tools for embedded systems [ramsey:lctes:1998]
  • Specifying representations of machine instructions [ramsey:toplas:1997]
  • The New Jersey machine-code toolkit [ramsey:usenix:1995]
  • HOIST: a system for automatically deriving static analyzers for embedded systems [regehr:asplos:2004]
  • Eliminating stack overflow by abstract interpretation [regehr:emsoft:2003]
  • Deriving abstract transfer functions for analyzing embedded software [regehr:lctes:2006]
  • Eliminating stack overflow by abstract interpretation [regehr:tecs:2005]
  • End-to-end verification of ARM processors with ISA-formal [reid:cav:2016]
  • Trustworthy specifications of ARM v8-A and v8-M system level architecture [reid:fmcad:2016]
  • Who guards the guards? Formal validation of the ARM v8-M architecture specification [reid:oopsla:2017]
  • Defining interfaces between hardware and software: Quality and performance [reid:phd:2019]
  • Formally verified big step semantics out of x86-64 binaries [roessle:cpp:2019]
  • A machine description facility for compiler testing [samet:ieeetse:1977]
  • Automatically proving the correctness of translations involving optimized code. [samet:phd:1975]
  • ZSim: Fast and accurate microarchitectural simulation of thousand-core systems [sanchez:isca:2013]
  • Understanding POWER multiprocessors [sarkar:pldi:2011]
  • The semantics of x86-CC multiprocessor machine code [sarkar:popl:2009]
  • Integrated semantics of intermediate-language C and macro-assembler for pervasive formal verification of operating systems and hypervisors from VerisoftXT [schmaltz:vstte:2012]
  • ARM Architecture Reference Manual (ARMv5 edition) [seal:book:2000]
  • CompCertTSO: A verified compiler for relaxed-memory concurrency [sevcik:jacm:2013]
  • Translation validation for a verified OS kernel [sewell:pldi:2013]
  • Certification of an instruction set simulator [shi:phd:2013]
  • ARMv8-A system semantics: Instruction fetch in relaxed architectures [simner:pls:2020]
  • A survey of computer hardware description languages in the U.S.A. [su:computer:1974]
  • Program verification in the presence of cached address translation [syeda:itp:2018]
  • A new verified compiler backend for CakeML [tan:icfp:2016]
  • Formal verification of a multiprocessor hypervisor on Arm relaxed memory hardware [tao:sosp:2021]
  • Opening Pandora's box: A systematic study of new ways microarchitecture can leak private data [vicarte:isca:2021]
  • CHERI: A hybrid capability-system architecture for scalable software compartmentalization [watson:sandp:2015]
  • Automatic generation and validation of instruction encoders and decoders [xu:cav:2021]
  • Raising binaries to LLVM IR with MCTOLL (WIP paper) [yadavalli:lctes:2019]
  • Integrating memory consistency models with instruction-level abstraction for heterogeneous system-on-chip verification [zhang:fmcad:2018]
  • LISA – machine description language and generic machine model for HW/SW co-design [zivojnovic:vlsi:1996]
  • Solver aided reverse engineering of architectural features [zorn:iscawddd:2017]