Anonymous user
User:Realazthat/Projects wishlist/LLVM/Formal methods: Difference between revisions
User:Realazthat/Projects wishlist/LLVM/Formal methods (view source)
Revision as of 04:19, 1 November 2010
, 13 years agono edit summary
(Created page with '==Formal methods project== Write an LLVM pass that will prove certain properties of functions. ==Features== Things that the pass might prove, for each function: * That all '''as…') |
No edit summary |
||
(6 intermediate revisions by the same user not shown) | |||
Line 1:
==Features==
Follow the examples of [[wp:Java_Modeling_Language]] and [[wp:SPARK_programming_language]].
Things that the pass might prove, for each function:
* That all '''assert''' statements can not occur, or complain otherwise (if an '''assert''' statement cannot be proved to not fail)
Line 8:
* Determine if the function requires Turing-completeness
** [[wp:Termination_analysis]]
** Reduction of turing-ness if possible (if provable) to decidable
** Do some '''good stuff''', as the function is not Turing-complete
** Equivalence?
Line 14 ⟶ 15:
*** http://www.cs.nott.ac.uk/~nad/publications/ => http://www.cs.nott.ac.uk/~nad/publications/danielsson-popl2008.pdf
*** [http://research.microsoft.com/en-us/um/cambridge/projects/terminator/ Microsoft Terminator] (sounds insidious).
* Compute function complexity (best, average, worst) of an algorithm (function)
** Allow the function to assert complexity
* Allow arbitrary restrictions on functions, which would propagate through the call graph
** Complexity (time/memory)
** Restricting stack allocation
** Restricting heap allocation
* Allow a programmer to make certain assumptions on input (probably through assertions)
* Prove that no '''undefined behavior''' can occur
** Math overflows/underflows
** Out of bounds access
** Memory leaks
** Dangling pointers
*** etc.
** Null dereferencing
** What else
* Determine valid input ranges (if the type of the input does not already assert this)
* Show proofs for all of the above
** Create [[wp:Proof-carrying_code| Proof-carrying code]]
* Impossible stuff
** Be able to calculate a function inverse if possible
**: Hmmmm
** Transformation of function to set of equivalent functions
**: Hmmmm
* Side effect free functions
* Pure functions
* Reentrant functions
* No deadlocks etc.
* If any of the above can't be proven, show test counter examples; that is exploitable input
** Related
Line 34 ⟶ 50:
*** [http://seanhn.wordpress.com/2010/07/17/applying-taint-analysis-and-theorem-proving-to-exploit-development/ Applying Taint Analysis and Theorem Proving to Exploit Development]
***: Another blog post, by thesis author
|