« BACK TO PROGRAM

Proving security properties in software of unknown provenance

Ben Hocking - Dependable Computing

In the safety and security community, everyone knows that the best time to include formal analysis of your desired properties is at the very beginning. If formal methods are not involved during requirements analysis, or during the specifications phase, then at least one should apply formal methods during the implementation phase.

However, what if one is using Software of Unknown Provenance (SOUP) after all of these phases have already passed? Has the safety/security "horse" already left the stable?

Techniques used to ensure SOUP has desired properties include sandboxing and/or altering the binary code after the fact to catch potential violations of the properties one wishes to enforce. However, these approaches can add memory or latency overhead to the executable that might not be acceptable, especially for embedded systems.

A model of the X86 architecture in SPARK Ada, along with a system for translating binaries into a SPARK Ada representation that uses this model, allows for the proof of these desired security properties. This enables binary modification to be limited to parts of the binary that cannot be proven to have the desired properties.

Download this presentation

About Ben Hocking

Dr. Hocking is a principal scientist at Dependable Computing specializing in formal methods and safety cases. Dr. Hocking earned his PhD and Masters in Computer Science from the University of Virginia, an MS in Physics/Astronomy from Georgia State, and a BS in Physics from Georgia Tech.