Menu
The role of formal methods in securing low-level software components and TEEs
Semiconductors are at the core of many things we see around us: from game consoles, mobile devices, smart meters to automotive vehicles to aircrafts and equipment used in industrial settings and mission critical domains such as space and defense. How critical semiconductors are, is made evident from the recent shortage that has brought the automotive industry to a standstill. It shows how much impact they can have on an entire vertical. Having said that, with the proliferation of consumer electronic devices, IoT equipment in homes, in industrial settings, and automotive vehicles; semiconductors continue to see growth, with well over a trillion of them sold annually. While this is an impressive number, it also brings with it some very serious challenges when it comes to the security of millions or rather billions of devices.
Vulnerabilities in low level software components, part of these semiconductors, can expose these devices to security threats that can have very serious consequences. There is some information to substantiate that, over the last five years alone related vulnerabilities have gone up by over 573% and 80% of the enterprises have seen at least one firmware attack in the past two years. There are very well-known incidents where software issues have exposed millions of mobile devices to security threats. Cyber-attacks on critical infrastructure are on the rise as well. The common denominator in all these examples are the vulnerabilities in the low-level software components that are exploited. These are components such as drivers, kernels, real time operating systems and TEEs. What does this mean? This means that preventing device level attacks that are targeting these low-level software components is extremely critical and is at the forefront of cybersecurity.
While traditional methods and tools are used for finding potential issues and cannot prove complete absence of bugs, this is something that TrustInSoft Analyzer can deliver. TrustInSoft analyzer is an advanced C and C++ source code analyzer that delivers a mathematical proof by leveraging advanced static and dynamic analysis techniques, combined with formal methods to ensure that low level code is secure and reliable and offers the highest quality. There are no guesses or list of potential issues, what you get is a mathematical guarantee by proving the absence of all undefined behaviors.
Undefined behaviors, as explained precisely in the C and C++ standards, can be very complex and troublesome if not detected early on. It can lead to serious consequences such as unpredictable results or software crashes. In turn, this can lead to even bigger problems. Undefined behaviors can also be exploited by hackers to trigger Arbitrary Code Execution. So by guaranteed absence of errors, such as buffer overflow, integer overflow, division by zero, for example, early on in the software development lifecycle, you can address and eliminate potential issues that might arise during runtime. By mathematically proving correctness you can ensure that the code performs the way it is supposed to, and rest assured that the firmware code is secure.
What is the secret behind this? Simply put, the secret is the tool’s ability to perform thanks to formal methods: an equivalent of large number of tests in a short span of time to assess all the possible behaviors of the code that has been analyzed. By doing that, we are able to prove absence of vulnerabilities.
Here are a few points that highlight why traditional methods and techniques may not be sufficient when it comes to security of low-level code. Traditional analyzers are generally unsound. Meaning that they do not report all problems. TrustInSoft Analyzer performs sound code analysis by ensuring that if a bug exists in the code, the tool will not sit quietly and will indeed raise an alarm. Traditional approaches perform, for the most part, syntactic analysis merely searching for patterns or suspicious code constructs to deliver a list of potential bugs that may or may not be real and a large number of false positives.
TrustInSoft Analyzer applies formal methods and performs semantic analysis of the code analyzing its behavior and checking execution for all possible values to identify issues and guarantee the absence of all undefined behavior. This results in low level code that is secure and very high quality. What are some of the examples of this low-level code? We’ll explore three different use cases where TrustInSoft was able to prove the security of this low-level software.
The first one is a unique and one of its kind result, which is based on the ARM Mbed TLS stack at the core of the ARM Mbed environment. The analysis performed using TrustInSoft Analyzer has demonstrated how the stack is immune to vulnerabilities such as buffer overflow.
This was a very unique result. The NIST, which is the National Institute of Standards and Technology, in its report to the White House, mentioned the technology and the fact that TrustInSoft performed a mathematical assessment of absence of entire families of vulnerabilities on ARM Mbed TLS.
The second example was an assessment performed on a device driver. In this case, a driver for a digital output motion sensor from STMicroelectronics primarily used in automotive applications. Here again the driver code was analyzed using TrustInSoft Analyzer and within the perimeter of the defined tests, through exhaustive analysis, the tool was able to mathematically guarantee that for any given input and execution path there was no undefined behavior. The key takeaway here is that it was performed within a short period of time. The analyzer was able to identify an issue, which was buffer overflow. Once corrected the analyzer confirmed that for all existing tests, the driver had no undefined behavior.
The third example is a Linux kernel driver for the Goodix capacitive flagship, which is widely used in mobile phone devices. Here, a formal analysis was performed on the kernel driver using the analyzer and within the perimeter of the analysis the tool was able to assess that the driver is secure from a large number of vulnerabilities that could compromise the complete OS. This was indeed an interesting use case for a chip that is widely used in mobile devices and could be compromised if a hacker could simulate a screen touch with multiple fingers or inputs in that situation. The question was, is the kernel driver robust enough to sustain such an attack? TrustInSoft was able to assess the immunity of the current driver for vulnerabilities within the parameter of the analysis.
Finally, Trusted Execution Environments (TEEs) are known to be key to ensure the security of devices, but there have been incidents where vulnerabilities within the TEEs themselves have exposed the chipsets and devices to security breaches. The security of TEEs is very critical, not just for the semiconductor manufacturer, but also domains that are heavily dependent on semiconductors such as telecom, mobile consumer devices and automotive. TrustInSoft Analyzer delivers TEE security by detecting critical firmware vulnerabilities early in the development cycle and providing a mathematical guarantee.
The real differentiator is a unique methodology that incrementally and progressively helps you achieve a high firmware quality consisting of a three-phase approach. The first stage is what we call interpreter mode, or level one. At this level, TrustInSoft Analyzer simply repeats existing tests. The analyzer exhaustively detects undefined behavior. It will help you find bugs that are very subtle, which otherwise may not be found. In other words, it helps you get the most out of your existing tests. Every bug identified is a real bug, so there’s zero false positives or false negatives, what you see is real and you get a mathematical guarantee that all undefined behaviors are detected for your existing tests.
Moving on to level two, which is the analyzer module that can progressively increase the number of tests that you can do to reach an exhaustive coverage by generalizing the inputs. You can conduct the equivalent of a very large number of tests and mathematically guarantee that your code does not have any undefined behavior for any input so you still have zero false negatives, and you can achieve up to 100% coverage on critical functions.
Finally, you can do a functional proof proving that a piece of low-level C and C++ code is doing exactly what it is supposed to do. It takes more time, but you can guarantee that the software specifications are indeed enforced on the code.
TrustInSoft Analyzer empowers the developers and testers, enabling them to find and fix the undefined behaviors, using their existing tests. Additionally, boosting the software coverage by performing the equivalent of a large number of tests with one generalized input so that you can progressively reach a higher quality and finally get a mathematical guarantee on the absence of undefined behavior, thus ensuring the absence of crashes, vulnerabilities, and the deterministic behavior and the security of your low-level code.
So, how does TrustInSoft help their customers? The primary value that TrustInSoft delivers is the improvement of operational efficiency by reducing the software test coverage costs by optimizing the bug identification and remediation, essentially focusing on what’s real.
Number two, TrustInSoft helps generate revenue opportunities by positioning security as a feature to gain market share, to get to the right certification level, and to secure time to market sensitive opportunities.
Finally, TrustInSoft helps to control the human and financial risks by preventing issues from occurring in the field.
Learn more about TrustInSoft Analyzer: https://trust-in-soft.com/product/trustinsoft-analyzer/
