Secure Coding mailing list archives
static analysis you say?
From: ge at linuxbox.org (Gadi Evron)
Date: Thu, 09 Feb 2006 08:08:54 +0200
Just last month Greta Yorsh, fresh from work in Microsoft Research over in the US lectured to us on something related in TAUSEC (http://www.cs.tau.ac.il/tausec - in Hebrew). ----- Title: Testing, Abstraction, Theorem Proving: Better Together. We present a method for static program analysis that leverages tests and concrete program executions. State abstractions generalizes the set of program states obtained from concrete executions. A theorem prover is then used for checking that the generalized set of concrete states covers all potential executions, and satisfies additional safety properties. Our method finds the same potential errors as the most-precise abstract interpreter for a given abstraction, and potentially more efficient. Additionally, it provides a new way to tune performance by alternating between concrete execution and theorem proving. ----- Anyone follow that? I didn't. VERY basically put, she showed a system that was developed over 5 years that abstracts static code such as of device drivers to a simple boolean program, and then follows the code to find errors. Later comparing these errors to a run on a tad less abstracted program to see if the error is really there. ^^^ That is probably the worst description you will ever hear of SLAM. She claims that with her research (not SLAM) she can prove mathematically a program is secure.. erm. She was a very impressive lecturer and almost convinced me, I really was impressed. Here are some links from her lecture (ignore the first line which is in Hebrew): http://www.cs.tau.ac.il/tausec/lectures/Greta_Yorsh_links.html Gadi.
Current thread:
- static analysis you say? Gadi Evron (Feb 08)