User:Realazthat/Projects wishlist/LLVM/Formal methods

Formal methods project

Write an LLVM pass that will prove certain properties of functions.

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
  • 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

    • http://www.cs.nott.ac.uk/~nad/publications/ => http://www.cs.nott.ac.uk/~nad/publications/danielsson-popl2008.pdf
    • Microsoft Terminator (sounds insidious).
• Compute function 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)
• 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

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

  • SLAM, by MS, has 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

• 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