SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Compilation

Research Corner - Sensitive Data Sanitization for SPARK

by Yannick Moy in Compilation, Formal Verification, Papers and Slides – June 20, 2017

Well-known SPARK expert and advocate Rod Chapman presented at the latest Ada Europe conference a paper on "Sanitizing Sensitive Data: How to get it Right (or at least Less Wrong...)". Rod's work in the latest years has switched to more security-focused topics it seems, and this work is attacking a subtle problem with new ideas. Definitely worth reading.

How Our Compiler Learnt From Our Analyzers

by Yannick Moy in Compilation, Formal Verification – May 22, 2015

Program analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent with the way that the compiler interprets it to generate an executable, or the information computed is irrelevant, possibly misleading. For example, if the analyzer says that there are no possible run-time errors in a program, and you rely on this information to compile with dynamic checking off, it is crucial that no run-time error could occur as a result of a divergence of opinion between the analyzer and the compiler on the meaning of an instruction. We recently discovered such an inconsistency in how our compiler and analyzers dealt with floating-point exponentiation, which lead to a change in how GNAT now compile these operations.