User:Realazthat/Projects wishlist/LLVM/Formal methods: Difference between revisions
Content added Content deleted
No edit summary |
|||
(3 intermediate revisions by the same user not shown) | |||
Line 1: | Line 1: | ||
==Formal methods project== |
|||
Write an LLVM pass that will prove certain properties of functions. |
|||
==Features== |
==Features== |
||
Follow the examples of [[wp:Java_Modeling_Language]] and [[wp:SPARK_programming_language]]. |
|||
Things that the pass might prove, for each function: |
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) |
* That all '''assert''' statements can not occur, or complain otherwise (if an '''assert''' statement cannot be proved to not fail) |
||
Line 8: | Line 8: | ||
* Determine if the function requires Turing-completeness |
* Determine if the function requires Turing-completeness |
||
** [[wp:Termination_analysis]] |
** [[wp:Termination_analysis]] |
||
** Reduction of turing-ness if possible (if provable) to decidable |
|||
** Do some '''good stuff''', as the function is not Turing-complete |
** Do some '''good stuff''', as the function is not Turing-complete |
||
** Equivalence? |
** Equivalence? |
||
Line 14: | Line 15: | ||
*** http://www.cs.nott.ac.uk/~nad/publications/ => http://www.cs.nott.ac.uk/~nad/publications/danielsson-popl2008.pdf |
*** 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). |
*** [http://research.microsoft.com/en-us/um/cambridge/projects/terminator/ Microsoft Terminator] (sounds insidious). |
||
* Compute function complexity |
* Compute function complexity (best, average, worst) of an algorithm (function) |
||
** Allow the function to assert complexity |
** 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) |
* Allow a programmer to make certain assumptions on input (probably through assertions) |
||
* Prove that no undefined behavior can occur |
* Prove that no '''undefined behavior''' can occur |
||
** Math overflows/underflows |
** Math overflows/underflows |
||
** Out of bounds access |
** Out of bounds access |
||
** Memory leaks |
|||
** Dangling pointers |
|||
*** etc. |
|||
** Null dereferencing |
|||
** What else |
** What else |
||
* Determine valid input ranges (if the type of the input does not already assert this) |
* Determine valid input ranges (if the type of the input does not already assert this) |
||
* Show proofs for all of the above |
* Show proofs for all of the above |
||
** Create [[wp:Proof-carrying_code| Proof-carrying code]] |
** Create [[wp:Proof-carrying_code| Proof-carrying code]] |
||
* Impossible stuff |
|||
* Be able to calculate a function inverse if possible |
** Be able to calculate a function inverse if possible |
||
*: Hmmmm |
**: 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 |
* If any of the above can't be proven, show test counter examples; that is exploitable input |
||
** Related |
** Related |
||
Line 34: | Line 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] |
*** [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 |
***: Another blog post, by thesis author |
||
==Test examples== |
|||
* Prove that a regular expression evaluator halts (IE. calculate the computational complexity). |
|||
==Reference material== |
|||
* [[wp:Correctness_(computer_science)]] |
|||
* [[wp:Declarative_programming]] |
|||
* http://www.jaist.ac.jp/~hirokawa/tool/ |
|||
*: A pretty comprehensive page about whats out there in the proving world |
|||
* [[wp:Constraint_programming]] |
|||
*: How does this relate? |
|||
== Further reading == |
|||
Read this stuff: |
|||
* http://www.csci.csusb.edu/dick/papers/rjb93a.xbnf.html |
|||
===Implementation methods=== |
|||
* [[wp:Hoare_logic]] |
|||
* [[wp:Agda_(theorem_prover)]] |
|||
* [[wp:Automated_theorem_proving]] |
|||
===SMT Research=== |
|||
* http://research.microsoft.com/en-us/um/people/leonardo/lab.pdf |
|||
* SMT solver |
|||
** http://www.cs.virginia.edu/~weimer/2007-615/lectures.html |
|||
**: ddunbar on #llvm suggested reading for SMT |
|||
* www.key-project.org/keysymposium10/slides/Falke_LLBMC.pdf |
|||
*: Another paper with details about LLVM => SMT |
|||
* BLAST, SLAM, and PREfast |
|||
*: ddunbar mentioned these as similar to this project |
|||
** [http://research.microsoft.com/en-us/projects/slam/ SLAM], by MS, has [http://research.microsoft.com/pubs/121290/axioms.submitted.pdf a paper] which has the same idea for representing memory in SMT |
|||
* Slide show demonstrating same project, using LLVM: http://events.iaik.tugraz.at/avm2008/EvdinTorok_StaticMemoryAccessChecking.pdf |
|||
==Related work== |
|||
* [http://llvm.org/pubs/2007-SOSP-SVA.pdf LLVM Secure Virtual Architecture] |
|||
* [http://www.cs.cornell.edu/talc/ Typed assembly language] |
|||
* Native Client? |
|||
* [http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf Total Functional Programming] |
|||
*: Paper that argues for [[wp:Total Functional Programming|Total Functional Programming]] |
|||
* http://www.cs.umd.edu/~saurabhs/pacs/ |
|||
*: '''Program verification specs using SMT solvers''' |
|||
==Non-Turing-complete languages== |
|||
* [[wp:BlooP_and_FlooP]] |
|||
* [[wp:Charity_(programming_language)]] |
|||
* [[wp:Epigram_(programming_language)]] |
|||
* [http://www-fp.cs.st-andrews.ac.uk/hume/index.shtml The Hume Programming Language] (Higher-order Unified Meta-Environment) |
|||
*: Five layers of progressively more complete, and progressively less safe, languages, see the [http://www-fp.cs.st-andrews.ac.uk/hume/report/hume-report.pdf Hume Report] |
|||
==Other interesting languages== |
|||
* [[wp:UNITY_(programming_language)]] |
|||
*: No flow control; seems very declarative |
|||
* [http://wiki.portal.chalmers.se/agda/pmwiki.php Agda] |
|||
*: Requires termination proofs, effectively making it decidable (I think) |
|||
** Also a theorem proover (can be a language and its proof according to the [[wp:Curry–Howard_correspondence#Related_proofs-as-programs_correspondences| Curry–Howard correspondence]] |
Latest revision as of 04:19, 1 November 2010
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)
- LLVM and assert/assume: http://llvm.org/bugs/show_bug.cgi?id=810
- 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?
- Allow a function to assert only co-recursion (no requirement for Turing-completeness)
- Probably requires that the function is rewritable in non-Turing-complete, and thus requires that the function not require Turing-completeness
- 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 Proof-carrying code
- Impossible stuff
- Be able to calculate a function inverse if possible
- Hmmmm
- Transformation of function to set of equivalent functions
- Hmmmm
- Be able to calculate a function inverse if possible
- 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
- http://seanhn.files.wordpress.com/2009/09/thesis1.pdf
- A thesis on finding exploiting input using SMT
- Fun uses for an SMT solver
- Using SMT to find exploitable input, blog post, by thesis author
- Applying Taint Analysis and Theorem Proving to Exploit Development
- Another blog post, by thesis author
- http://seanhn.files.wordpress.com/2009/09/thesis1.pdf
- Related