User:Realazthat/Projects wishlist/LLVM/Formal methods: Difference between revisions
Content added Content deleted
No edit summary |
No edit summary |
||
Line 22: | Line 22: | ||
** Restricting heap 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 |
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