See you at BlackHat USA


Why Exhaustive Static Analysis is the key to validating a secure and reliable Trusted Execution Environment

This post is Part 3 of a 3-part series derived from TrustInSoft’s latest white paper, “How Exhaustive Static Analysis Can Prove the Security of Trusted Execution Environments.” To obtain a FREE copy, CLICK HERE.

Exhaustive static analysis to validate a secure and reliable TEE, Part 3 of 3


In Part 1 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 eliminated from a piece of code.

In Part 2, we looked at why safetycritical industries like aerospace and nuclear energy generation moved away from traditional software testing two decades ago and why developers of TEEs need to follow a similar path today.

In this final installment of our series, we’ll explore a new technology called exhaustive static analysis. We’ll examine what it is, what it does, its major benefits, and why it is critical for the successful validation of trusted execution environments.

Exhaustive Static Analysis – guaranteeing trust in your trusted execution environment

The key to guaranteeing the trustworthiness of your TEE is exhaustive static analysis.


Exhaustive static analysis is a methodology that makes use of a variety of formal methods techniques to answer the questions users ask about their code. It takes know-how developed to guarantee the behavior of safety-critical systems and expands its scope to guarantee data security as well as safety and functionality. It makes that know-how available to all developers for use in the development of any device—from smartphones to game consoles, medical technology to remote monitoring devices.


Exhaustive static analysis is also a framework where many formal methods collaborate. It contains algorithms that choose the correct formal method according to the question being asked. And it can switch seamlessly from one formal method to another, depending on the problem it has been asked to solve.


In other words, exhaustive static analysis is a holistic approach, not one of brute force. Rather than trying to solve every problem using a single formal method, the framework has been designed to determine which formal method or combination of formal methods is best suited to solving the problem at hand and to apply those methods in the best way possible.

Plugs right into your existing development process

What’s more, exhaustive static analysis does all this in a way that does not disrupt the normal software development process. It brings the value of mathematical formal methods to software development in a way that’s practically invisible to the developer.


With an exhaustive static analysis framework, all the aforementioned selection and application of formal methods are transparent to the developer. Users are simply testing their code in a manner very similar to what they’re already accustomed to.


The framework expands and automates the testing process. For example, by adding just a couple of lines of code to your test script, you can expand a limited set of test cases to a complete set of test cases covering the complete range of possible values for all input variables.


Again, you don’t need a Ph.D. in formal methods to use these tools. Any developer can handle them. Users don’t even need to be aware of the method the tool is using. They just express the problem and the tool does the analysis automatically. It’s extremely easy for users to find answers. The framework chooses the right tools for the problem and switches tools on the fly.


For example, our own platform, TrustInSoft Analyzer for C and C++, employs several abstract memory models to analyze the software being validated. This process is completely hidden from users. They needn’t know anything about them.


TrustInSoft Analyzer has been designed and developed so that no matter how a C/C++ developer programs, it will extract the meaning of the code so that the right formal methods are applied. It was cited in a National Institute of Standards and Technology report to the White House for having demonstrated that it can be used to formally guarantee that (1) no known undesired behaviors (bugs) are present in a system and that (2) the system behaves exactly according to its specification.3

The major benefits of exhaustive static analysis

Using exhaustive static analysis, you can guarantee the absence of coding flaws—like buffer overflows—that hackers exploit. That means it’s now possible to end the cat-and-mouse game of hackers finding vulnerabilities and developers scrambling to remove them. With exhaustive static analysis, you can eliminate all such flaws before hackers even have the chance to look for them.


You’ll eliminate many flaws conventional tools fail to catch. For example, using TrustInSoft Analyzer, existing test scripts downloaded from GitHub, and a fuzzer, we recently uncovered thirteen undefined behaviors (UB) in the popular, open-source network protocol analyzer and IP packet sniffer Wireshark (Figure 1) 4. These flaws had been in the Wireshark code for years, left undiscovered by other tools.

Image: List of previously undetected bugs in Wireshark. In 2019, 13 UBs were identified on Wireshark Packet Analyzer. New bugs were found that were not caught by other tools for years. Rules of the game: Find UBs by replaying-existing test suits & use a fuzzer (AFL). Results: After generating 10,000 tests with AFL from the 44 existing ones, we found 13 UBs. These were uninitialized variables (3335 times), incompatible function pointer (735), uninitialized variable (10), uninitialized variable (63), signed overflow (15) and so on.

Figure 1: Previously undetected bugs uncovered in Wireshark

Then, if you want to go a step farther, you can guarantee the absence of complete families of vulnerabilities in your code, through exhaustive coverage.


Exhaustive static analysis enables companies to guarantee to customers and regulatory bodies that their applications are completely free of coding flaws and conform exactly to their functional requirements. These guarantees are critical in a TEE.


One other benefit of exhaustive static analysis: developer satisfaction.


Exhaustive static analysis helps developers perfect the applications they’ve worked so hard to create. It helps them quickly find and eliminate those subtle coding errors that are so easy to make without even being aware of them… and that are so hard to track down after they’ve been made. It saves developers time. It makes them feel great about what they’ve built.


Plus, it does all this in an automated, fully-comprehensive manner. Exhaustive static analysis finds all the needles in your haystack.

The bottom line

A trusted execution environment needs to work securely and flawlessly.  Traditional software testing methods are inadequate to the task of TEE development and offer no guarantee of security or reliability.

Exhaustive static testing, on the other hand, can provide guarantees that your TEE is secure, 100% free of defects that hackers can exploit, and behaves exactly as specified.

If you have enjoyed this post and would like to have 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, we also look briefly at a couple 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 3 of a 3-part series derived from TrustInSoft’s latest white paper, “How Exhaustive Static Analysis Can Prove the Security of Trusted Execution Environments.” To obtain a FREE copy, CLICK HERE.


 Black, P.; Badger, L.; Guttman, B.; Fong, E.; Dramatically Reducing Software Vulnerabilities: Report to the White House Office of Science and Technology Policy; National Institute of Science and Technology (NIST), November 2016.

2 Bakker, P.; Providing assurance and trust in PolarSSL; May 2014

3 Regehr, J.; Comments on a Formal Verification of PolarSSL, September 2015.

4 Zupkus, A; The Wireshark Challenge: how to ensure the security of open-source projects with formal methods; TrustInSoft, May 2020.


Related articles

June 18, 2024
June 4, 2024
May 31, 2024