Why exhaustive static analysis is ideally suited for ensuring the security of low-level code

January 16, 2023

In Part 1 of this series, we discussed why ensuring the security of low-level code—the code used in OS kernels, device firmware and other applications that interface directly with hardware—has become critical to the overall cybersecurity of embedded systems.

In Part 2, we examined why developers of low-level code need to go beyond traditional static analysis and software testing to verify that their applications are free from coding defects that can be exploited by hackers.

In this final installment, we reveal why exhaustive static analysis—the method employed and automated by TrustInSoft Analyzer—is ideally suited to ensuring the security of low-level code.

This post is Part 3 of a 3-part series derived from TrustInSoft’s latest white paper, “From Bare Metal to Kernel Code: How Exhaustive Static Analysis Can Guarantee Airtight Security in Low-level Software and Firmware” To obtain a FREE copy, CLICK HERE.

We concluded our previous post by asking the following question: If conventional static analysis and software testing are inadequate for guaranteeing the security of low-level code, how can companies protect themselves? What can they do instead?

For many, the answer is exhaustive static analysis.

Exhaustive static analysis and its zero-defect guarantee

Exhaustive static analysis is an alternative to traditional static analysis. Rather than sets of rules, exhaustive static analysis uses mathematical formal methods to prove unequivocally that your code is free from coding errors and undefined behaviors that hackers can exploit.

The method was initially developed for formal verification of safety-critical systems, like those of the aerospace industry, where a software failure could result in the destruction of property and the loss of human life. Having evolved over nearly two decades of refinement, it is now approved for use in place of software testing for the certification of airborne systems under DO-178C, the aerospace industry’s de facto standard for software certification.[i]

Exhaustive static analysis is a methodology that makes use of a variety of formal methods 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 cybersecurity 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, from medical technology to remote monitoring devices.

Exhaustive static analysis is also a framework where a broad range of formal methods collaborate as one. Its tools contain algorithms that choose the right formal method according to the question being asked. A good exhaustive static analysis tool 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.

Ideally suited to low-level code

Software for safety-critical aerospace apps historically ran on bare metal—directly on the hardware—with no OS in between. This was done primarily for two reasons.

The first is speed. Real-time operational flight programs like those used in flight control, navigation and weapon control systems must be able to react very quickly to changing inputs from pilots and sensors.

The second reason is memory limitation. Aircraft and spacecraft don’t have access to massive servers or cloud storage. Low-level embedded code has to make do with the memory chips it has in its own box. To deal with these constraints, programmers often have to resort to non-standard coding structures to make the code run as efficiently as possible.

Having been developed to verify software in safety-critical systems, exhaustive static analysis is ideally suited to verifying low-level code.

As mentioned earlier, traditional static analysis tools are not designed to deal with these complex, non-standard structures. In contrast, exhaustive static analysis tools, having evolved in the aerospace sector, were designed to look at the code the way the hardware sees it. For example, our tool, TrustInSoft Analyzer, has specific features that enable you to specify precisely the hardware characteristics and the toolchain. Based on this configuration, TrustInSoft Analyzer sees the software product as it will be and run on the final hardware.

Sound tools

Exhaustive static analysis tools are what are called “sound” in the context of formal methods. That is, they are designed so they will not miss a single defect and can be used to guarantee that a software program is completely free of bugs and security vulnerabilities. They can even be used to guarantee that the program complies exactly with its specification.

By being just as precise as the code’s compiler, these tools are able to thoroughly understand complex low-level code and perform precise mathematical analyses on it.

Also, since the formal methods employed in exhaustive static analysis are mathematical proving techniques rather than discrete test cases, they can be applied to wide ranges of input values all at once. The iterative application of different sets of input values performed in traditional software testing is not required when using formal methods. Ultimately, exhaustive static analysis saves a lot of time in verification.

Designed so any developer can use them easily

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.

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

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

Again, you don’t need a PhD in formal methods to use these tools. Any developer can handle them. In most cases, users don’t even need to be aware of the method the tool is using. They only need to test the code in a very similar way that they are already accustomed to.

For example, our own platform, TrustInSoft Analyzer for C/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[ii] for having demonstrated that it can be used to formally guarantee that no undesired behaviors (bugs) are present in a system.

Ideal for verifying OS kernels

Exhaustive static analysis can also guarantee the absence of vulnerabilities in an operating system. An OS is, after all, a bare metal program—one that provides layers of abstraction for the applications that run on top of it.

Developers of the operating systems used in many of today’s connected devices are finding it prudent and justifiable to use exhaustive static analysis to guarantee their OS is defect-free. This is true for those developing operating systems for their own products (like mobile phones and gaming consoles, for example), as well as for those who license an off-the-shelf OS (like real-time OS and hypervisors) for other manufacturers to use in the devices they produce.

At the moment, we have several customers who are so concerned about the security of their devices that they have chosen to develop their (micro) OS themselves. They use TrustInSoft Analyzer to verify the security of that OS.

Clearly, the next step is for device manufacturers to demand that the off-the-shelf operating systems they are licensing from third parties are guaranteed to be free of all coding defects a hacker could exploit. Using TrustInSoft Analyzer, OS providers can provide that guarantee today.

For more information

If you found this post or others in this series useful, you may find it advantageous to download a free copy of the full white paper from which the series was derived.

From Bare Metal to Kernel Code: How Exhaustive Static Analysis Can Guarantee Airtight Security in Low-level Software and Firmware also includes two brief case studies on how our customers use TrustInSoft Analyzer to eliminate defects and ensure the security of their low-level code. Plus, you’ll find a guide for what to look for when choosing your own exhaustive static analysis solution.

Download the white paper

References

[i] Moy, Y., Ledinot, E., Delseny, H., Wiels, V., Monate, B., Testing or Formal Verification: DO-178C Alternatives and Industrial Experience, IEEE, April 2013.

[ii] 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.