Many users of Simulink and Embedded Coder target their applications to embedded systems. Embedded systems require high levels of integrity in their operation, and increasingly, these systems are being connected to networks to enable new functionality and provide monitoring capabilities. These extensions to embedded systems raise concerns about security vulnerabilities.

Our colleagues Jay Abraham and Corey Lagunowich saw the recent news stories about Apple's iOS security vulnerabilities, and looked a little closer at how to avoid these problems using Polyspace.

goto fail

Back in February, technology blogs and news outlets (see this article from The Guardian for an example) were abuzz about a newly discovered vulnerability in Apple’s iOS and Mac OS X. There was a problem in the Transport Layer Security (TLS) and Secure Sockets Layer (SSL) code that could be exploited by what is known as a Man in the Middle attack (MitM). The vulnerability was dubbed “goto fail”.

The Anatomy of the Defect

The defect originated in the TLS/SSL library in source file sslKeyExchange.c (accessible on www.opensource.apple.com). The stripped code snippet that represents the defect is shown in the screenshot below.

The problem with this code is that there are two repeated goto statements, and the second is not surrounded by an if statement. This means that any code after the second “goto fail” will never be executed (and is referred to as “unreachable code” or “dead code”). Therefore the function SSLHashSHA1.final() was never called. This scenario provided a set of conditions that could be exploited for an attack.

Presence, Not Absence

How do software bugs like this escape into production? In order to answer this question, let’s turn to the lessons taught by a founding member of the computer scientist community, Edsger W. Dijkstra.

Dijkstra is considered to be a leading contributor to the bedrock principles of computer science in the areas of programming languages and formal verification. Of all his tenets, perhaps the most famous is:

In theory, performing code review and executing the right set of test cases can catch most code defects. But this is hard in practice. Even for the simplest operations, such as adding two 32-bit integers, one would have to spend significant time to complete exhaustive testing. And if you don’t test for it – you won’t find it.

So how do we apply Dijkstra’s principle in order to develop safe and secure embedded systems? How do we show the absence of bugs? We use Static Code Analysis, like what is performed by Polyspace Bug Finder and Polyspace Code Prover.

Detecting Defects

How would Polyspace have stopped defects like these from being released? The screenshot below shows the results of Polyspace Bug Finder’s analysis on the code snippet. It flags the final if statement as dead code, because it cannot be reached.

The “goto fail” bug is a fairly straightforward example of this. What about something more complicated, something that requires being able to follow the data flow to detect? For that we can use Polyspace Code Prover.

A More Complex Example

The example below shows code where Polyspace Code Prover has flagged three items as not green (i.e. not proven reliable):

• Red: The while statement is flagged as red, because Polyspace has determined that the loop may not terminate before a run-time error occurs.
• Orange: That run-time error will be a divide-by-zero from line 13, which is why the division operator is flagged as orange.
• Grey: Relevant to our “goto fail” bug discussion is line 17, flagged as gray unreachable code. Why?

  Because Polyspace can follow the data flow, it knows that the if-statement on line 16 will always evaluate to false. If count ever did equal zero, a run-time error would have occurred on line 13 before the program reaches line 16. And Polyspace Code Prover can detect all this without requiring program execution, code instrumentation, or test cases.

  

  Takeaways

  The Apple “goto fail” is a teaching moment for embedded software engineers that develop and maintain critical automotive ECU, avionics, and medical devices. It highlights the need to augment code review and testing with static code analysis. You can look to Polyspace to scrutinize critical software components, find bugs, and ensure that no new bugs creep into your code.

  Give look at what Polyspace can do for you and let us know what you think by leaving a comment here.