Scalable translation validation of unverified legacy OS code

Amer Tahat, Sarang Joshi, Pronnoy Goswami, Binoy Ravindran
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 12 October 2019

Topic(s): os verification
Note(s): translation validation, Arm architecture, ASL, PVS theorem prover

Describes a toolchain for translation validation of radere2 reverse engineering tool using the ASL specification of the Arm architecture based on the PVS7 theorem prover.

Uses multiple techniques to validate translation of ASL to PVS7. Tested using 370 functions extracted from Linux and Google’s Zircon OS. Limited to loop-free leaf functions.