User:Realazthat/Projects wishlist/LLVM/Formal methods

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

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

• 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