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. The paper is available on Rod's blog. It was probably worth watching too, as anyone who has seen Rod in presentation knows, which was confirmed by the conference organizers who gave the best presentation award to his talk!

The use of pragma Inspection_Point to check the value of sanitized variable is something neat I think. His solution is both simple and powerful: he uses limited private types with a sanitization procedure marked No_Inline (to prevent inlining) to ensure that sensitive data cannot be copied around by the compiler in temporary variables or in registers, and to ensure that user-inserted sanitization won't be optimized away. Quite a clever use of Ada/SPARK features!

I also like the prospective idea of having the compiler sanitize the stack globally, saving the need for the user to insert calls to the sanitization procedure, which leaves the door open for missing calls and leaks of sensitive data. To be seen if we could add that to GCC/GNAT in the future.

Another idea that I'd like to investigate is whether some simple controlled types could make sense in a critical embedded context. Currently, controlled types are not supported by GNAT in this kind of context, where the Ravenscar SFP (Small Footprint) or Ravenscar full runtimes are used. But much of the complexity of controlled types comes from the need to call finalization procedures (equivalent to C++ destructors) when unwinding the stack as a result of an exception being raised. Since in many cases applications do not use the support of stack unwinding on exception (which is not supported anyway on Ravenscar SFP) but rather call what we call a "last chance handler" before restarting the application, maybe a version of controlled types for that context, without support for stack unwinding on exception, would be useful. Contact us if you'd like to push that idea!

comments powered by Disqus