[unicorn-engine] Formal assurance on unicorn ARMA64 emulations

  • From: Amer Tahat <antahat@xxxxxx>
  • To: unicorn-engine@xxxxxxxxxxxxx
  • Date: Mon, 4 Nov 2019 14:52:59 -0500

Hi All,

We want to share our paper from FMCAD19 with unicorn users,
http://theory.stanford.edu/~barrett/fmcad/papers/FMCAD2019_paper_77.pdf

Among many things, the paper describes a test generator and a formal
emulator based on a unicorn (AARCH 64) and ASL (ARM specification
language). We lift the formal semantics of the instructions to a theorem
prover PVS7 based on ASL. Then we generated tens of thousands of test cases
using unicorn for the instructions that we formalized. There was an
exciting match between the results obtained from the unicorn emulator and
their formal counterparts of ASL-based PVS7 models. The findings increase
the trust in the unicorn models as well as PVS7's.

The paper has formalized a subset of the instructions of AARCH64; more
details are involved in the article.

Enjoy!
-- 
Dr. Amer Tahat, Ph.D. CS&E
Systems Software Research Group,
454 Durham, Department of Electrical and Computer Engineering,
Virginia Tech University, Blacksburg, VA, 24061, U.S.A

Other related posts: