User:Realazthat/Projects wishlist/LLVM/Formal methods
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 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
- 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
- Allow the function to assert complexity
- 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
- 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
- Be able to calculate a function inverse if possible
- Hmmmm
- 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
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?
Implementation methods
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
- http://www.cs.virginia.edu/~weimer/2007-615/lectures.html
- 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
- Slide show demonstrating same project, using LLVM: http://events.iaik.tugraz.at/avm2008/EvdinTorok_StaticMemoryAccessChecking.pdf
Related work
- LLVM Secure Virtual Architecture
- Typed assembly language
- Native Client?
- Total Functional Programming
- Paper that argues for 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)
- The Hume Programming Language (Higher-order Unified Meta-Environment)
- Five layers of progressively more complete, and progressively less safe, languages, see the Hume Report
Other interesting languages
- wp:UNITY_(programming_language)
- No flow control; seems very declarative
- Agda
- Requires termination proofs, effectively making it decidable (I think)
- Also a theorem proover (can be a language and its proof according to the Curry–Howard correspondence