This post is Part 2 of a 3-part series derived from TrustInSoft’s latest white paper, “How Exhaustive Static Analysis can Prove the Security of TEEs” To obtain a FREE copy, CLICK HERE.
In the first post of this series, we discussed why the code of a trusted execution environment (TEE) needs to be completely free of undefined behaviors (bugs) and why traditional software testing cannot guarantee that every last bug has been eliminatedfrom a piece of code.
In this post, we’ll explore why industries like aerospace and nuclear energy generation—where much of the code needs to be flawless to assure safety—began moving away from traditional software testing some twenty years ago. We’ll look at where they moved and why, and we’ll examine why developers of modern, connected applications like TEEs need to follow a similar path and adopt a new generation of software validation tools.
Besides lacking a guarantee, traditional software has also proven to be a very expensive method for validating critical software—software that needs to be flawless—like that of a TEE.
In the aerospace and nuclear energy industries in the late 20th century, when traditional testing was the only available software validation option, software engineers spent much of their time reviewing their code by hand. They were keenly aware that an insidious bug might cost lives.
Since there were no tools that could guarantee their code would behave correctly, they combed through it line by line, looking for any coding irregularity that might result in undefined behavior. It was tedious. It took lots of time and energy and was extremely costly. Software engineers were stressed and got fed up. The turnover rate among them was very high, which added to the cost.
A study by the National Research Council in 2001 found that “The shortage of software engineers is an acute problem in the commercial and defense aerospace industry… High-potential young software engineers often leave for jobs in non-defense industries where pay scales are higher and perceived opportunities are more exciting.”1 Burnout from code review may have been a contributing factor.
By the end of the 1990s, it had become clear in safety-critical industries that software that had to be perfect needed new verification tools that could guarantee determinism and safety. Now, twenty years later, with the mass proliferation of both web-connected devices and cybercrime, it is clear that similar tools are needed in the development of trusted execution environments, as well as other applications tasked with protecting connected devices from cyberattacks.
At the beginning of this century, aerospace and nuclear engineers began looking toward formal methods. They spoke with researchers in the field. Their biggest question: “Could you help us guarantee the behavior of our code?”
Formal methods use mathematical techniques to “solve” the logic of computer programs or other systems (integrated circuits, for example) to answer questions about their behavior. For example, if you want to know if there is any way a buffer overflow could occur in your program, formal methods can be used to determine that. What’s more, a state-of-the-art formal methods tool can answer those questions for you automatically.
Formal methods are ideal for validating code that needs to be perfect. A sound formal methods tool will report every defect in your code. That may not sound so useful if you’re not worried about users finding bugs that can be fixed in a future release. But it’s highly useful if you’re developing a TEE that needs to be 100% reliable and impervious to cyberattacks.
Sound formal methods tools do more than just find bugs. When you do traditional testing, you can never be certain you didn’t forget an important test case. Formal methods, as we’ll see later, can guarantee you have exhaustive test coverage of your requirements.
Formal methods can also be used to guarantee your program exactly matches its specification. That doesn’t guarantee your application will work perfectly; there may be errors in the requirements. But your task then becomes reviewing the specification. That’s far easier than reviewing the full source code, as those poor aerospace-and-nuclear-sector software engineers used to do.
Widespread use of formal methods began in the semiconductor industry in the 1990s. Following the discovery of the Intel Pentium bug, Intel and the rest of the semiconductor industry began using a formal method called model checking to guarantee the functionality of their microprocessors before release.2
To use model checking, you first construct a model of your system. Then, you check the behavior of your model against its specification. Both the model of the system and its specification have to be formulated in some precise mathematical language. Modeling checking works fine when components are hardwired together, as when you have physical connections between transistors in a microprocessor. This method is still used in the semiconductor industry today.
Once you add software to your system, however, the situation becomes much more complicated. In software, rather than always having fixed connections between components, you can use pointers to address a vast number of memory addresses. The conceptual model for a microprocessor running software is much more versatile than that of the hardware itself because at any point in the program you can point to any memory location.
That ability for data or program flow to go anywhere makes it far more difficult to guarantee a system’s behavior. That’s why it’s so challenging to validate a TEE: a TEE can be just as complicated as an operating system. Very often, it is indeed an operating system in itself.
What’s more, programming styles can vary significantly within a TEE.
The separation kernel, which forms the basis of the TEE is written in very low-level code. It typically runs on bare metal, interfacing directly with the hardware. In contrast, the trusted applications within the TEE are written in a high-level style. They’re similar to typical applications, but they need to be completely bug-free. In the middle is a communication layer, such as VPN, which is written at a level somewhere in between that of the separation kernel and the trusted apps.
This variety of programming styles, along with system complexity, makes it impossible to validate a TEE using only a single formal method like model checking.
Fortunately, research in formal methods and the development of formal methods tools have evolved significantly since the mid-1990s. There now exist solutions that automatically choose and combine a full range of formal methods to find and eliminate software defects and formally validate software-based systems like TEEs.
Plus, in most cases, the selection and application of these formal methods are completely transparent to the user. You don’t need to be a formal methods expert. Any software developer can learn to use these tools quickly and easily.
In our next post, we’ll explore the benefits of this new generation of formal method tools in more detail.
If you prefer not to wait, or if you’d like to read the entire series in a more portable format, be sure to download our new white paper, “How Exhaustive Static Analysis Can Prove the Security of Trusted Execution Environments.” In the white paper, besides the content of this blog series, we look briefly at a pair of companies that have adopted this technology to validate trusted execution environments. Plus, we provide some tips on what to look for when choosing the solution that’s right for your organization. You can download your free copy here.
This post is Part 2 of a 3-part series derived from TrustInSoft’s latest white paper, “How Exhaustive Static Analysis can Prove the Security of TEEs” To obtain a FREE copy, CLICK HERE.
1 National Research Council; Review of the Future of the U.S. Aerospace Infrastructure and Aerospace Engineering Disciplines to Meet the Needs of the Air Force and the Department of Defense; The National Academies Press, 2001.
2 Clarke, E. M., Khaira M., Zhao, X.; Word Level Model Checking – Avoiding the Pentium FDIV Error; Proceedings of the 33rd Annual Conference on Design Automation Conference – DAC ’96. DAC ’96: 645–648.
