Abstract Interpretation and how to write secure software

Abstract interpretation is a method of static analysis. Static analysis is a method of checking for the correctness of the semantics of software. In particular abstract interpretation is a theory of sound approximation of the semantics of computer programs. Soundness in logic can be witnessed from the below example:

All men are mortal.
Socrates is a man.
Therefore, Socrates is mortal. 

This code example is also written in the example for Tauchain as Notation3 as:

:socrates :a :man .
{ ?x :a :man } => { ?x :a :mortal } .
fin.
?Y :a :mortal .
fin.

What is important to note here is that it is an example of a logical argument which is valid, which produces a clear conclusion. If A is true (Socrates is a man) , and if B is true (all men are mortal), then we can say B implies C (Socretes is a mortal). This reveals that the security gained through abstract interpretation comes from the strength of the logic behind the code.

The purpose of static analysis is the prevention of run time errors

Type checking provides security at the compile stage , and runtime error prevention strategies may require static analysis for use with imperative languages which do not have some of the features of the functional languages. Abstract interpretation is the verificaiton approach where you can be confident that there is proof of code reliability.

Because you can never have certainty, you instead must settle for approximation with regard to program behavior. When we remember that programs are proofs then we realize that underlying all proofs are logic. Bounded model checking can allow for the checking of the projected behavior of a program so as to rule out particularly dangerous behaviors through the use of formal constraints.

Software for C developers who want to use abstract interpretation can try Astree

• Astree:

Astrée aims at proving that the C programming language is correctlyused and that there can be no Run-Time Errors (RTE) during any execution in any environment.

I understand that this was no in depth, and only provides a superficial practical explanation. The goal here is to introduce the concept of abstract interpretation to more developers so that it can be utilized to produce more reliable code in cryptospace.

References

1. https://en.wikipedia.org/wiki/Abstract_interpretation#Sound_tools
2. http://www.astree.ens.fr/
3. https://web.stanford.edu/~bobonich/glances%20ahead/III.logic.language.html
4. https://en.wikipedia.org/wiki/Run_time_(program_lifecycle_phase)
5. http://www.mathworks.com/tagteam/72961_91517v01_white_paper_abstract_interpretation.pdf
6. http://www.di.ens.fr/~cousot/AI/IntroAbsInt.html
7. https://github.com/naturalog/tauchain/blob/master/examples/socrates