Dr. Eric W. Smith
|
|
||||
Dr. Eric W. Smith is the CEO of Kestrel Institute and is a Computer Scientist with over 20 years of experience in formal methods. He currently leads Kestrel’s DerivationMiner effort, which uses synthesis techniques (derivations, specifications, and refinements) to construct correctness proofs of code found in large online repositories. He co-leads Kestrel’s related APT (Automated Program Transformations) project, which is developing proof-emitting program transformations in the ACL2 theorem prover. APT technology has been used in several Kestrel projects, including DerivationMiner, Flex, and Trusted and Resilient Systems. At Kestrel, Dr. Smith is continuing to develop the Axe tool originally written for his Ph.D. thesis. Axe includes a high-performance rewriter, theorem prover, and equivalence checker and a tool to “lift” Java bytecode programs into ACL2 logical functions. Dr. Smith is extending the Axe lifter to apply to x86 binaries for the purpose of malware detection. Dr. Smith led Kestrel’s DARPA APAC effort to find malware in Android apps and formally prove correctness of apps without malware.
Before joining Kestrel, Dr. Smith completed his Ph.D. in Computer Science at Stanford University under Prof. David Dill. He wrote Axe, a theorem prover and equivalence checker capable of highly automated proofs about real-world cryptographic programs. Dr. Smith has extensive experience with the ACL2 theorem prover, using it for microprocessor verification at AMD and for processor modeling and machine code proofs at Rockwell Collins. Dr. Smith did his undergraduate work at the University of Texas at Austin, where he earned bachelor’s degrees in Computer Science and Plan II Honors under thesis advisor J Moore.
Tools: The tools I am working on these days include APT and Axe.
Selected publications:
Axe: An Automated Formal Equivalence Checking Tool for Programs. Eric W. Smith. Ph.D. Dissertation. Stanford University. 2011.
Automatic Formal Verification of Block Cipher Implementations. Eric Smith and David Dill. FMCAD ‘08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, November, 2008.
Formal Verification of Floating-Point RTL at AMD Using the ACL2 Theorem Prover. David Russinoff, Matt Kaufmann, Eric Smith, and Robert Sumners. 17th IMACS World Congress: Scientific Computation, Applied Mathematics and Simulation. July, 2005.
Meta Reasoning in ACL2. Warren A. Hunt, Matt Kaufmann, Robert Bellarmine Krug, and Eric Whitman Smith. 18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005, J. Hurd and T. Melham (eds.), Springer Lecture Notes in Computer Science, 3603, pp. 163–178, 2005.
A Robust Machine Code Proof Framework for Highly Secure Applications. David S. Hardin, Eric W. Smith, and William D. Young. ACL2 ‘06: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, 2006.
Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover, Eric Smith and Alessandro Coglio, Proc. 7th Working Conference on Verified Software: Tools, Techniques, and Experiments (VSTTE), 2015
A Versatile, Sound Tool for Simplifying Definitions, Alessandro Coglio, Matt Kaufmann, and Eric W. Smith. To appear in 14th International Workshop on the ACL2 Theorem Prover and Its Applications, 2017