User:Realazthat/Projects wishlist/LLVM/Formal methods: Difference between revisions

From Rosetta Code
Content added Content deleted
No edit summary
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]].
Follow the examples of [[wp:Java_Modeling_Language]] and [[wp:SPARK_programming_language]].
Line 11: 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 17: 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
* Allow arbitrary restrictions on functions, which would propagate through the call graph
Line 41: Line 39:
*** [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]]

Revision as of 02:47, 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
  • 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
    • What else
  • Determine valid input ranges (if the type of the input does not already assert this)
  • Show proofs for all of the above
  • 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
Retrieved from "https://rosettacode.org/wiki/User:Realazthat/Projects_wishlist/LLVM/Formal_methods?oldid=160424"