[unicorn-engine] Re: Formal assurance on unicorn ARMA64 emulations

  • From: Nguyen Anh Quynh <aquynh@xxxxxxxxx>
  • To: unicorn-engine@xxxxxxxxxxxxx
  • Date: Fri, 8 Nov 2019 16:13:01 +0800

Congrats on a nice work!

Feel free to put your paper up in the collection at
https://github.com/unicorn-engine/unicorn/issues/1104

Cheers,
Q

http://www.keystone-engine.org
http://www.capstone-engine.org
http://www.unicorn-engine.org


On Tue, Nov 5, 2019 at 3:54 AM Amer Tahat <antahat@xxxxxx> wrote:


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: