Should Have Used Ada (SHUA) #1 - Goto fail
Human society has a long tradition of designing and applying systems and technologies to limit the effects of our own inherent weaknesses. An early example is double-entry accounting; a system who's basic function is to catch common errors, and is more than 700 years old. Yet it is rare to find accountants who believe double-entry accounting should be abandoned, and replaced with something more error-prone but "convenient". Perhaps they recognize that the often tedious demands of double-entry accounting is exactly what makes it so reliable. Like most things in life, planning and care in the present pays off handsomely with stability and predictability in the future.
A common criticism of Ada includes a perceived excess verbosity. In fact, that was a deliberate design decision. Often in our rush to insert more and more programmer conveniences into our favourite languages, we tend to miss the raw human weaknesses that turn those shortcuts into unrelenting hazards.
Ada is perhaps the only mature, general-purpose language that began its life with a rigorously refined set of requirements that went through four revisions over three years, before any language design began. Those basic requirements live-on as the very first section of the Ada specification: "Design Goals". Many popular language standards lack any such broad statement of intent, let alone a thorough requirements discovery process that preceded the language design.
The "Should Have Used Ada" (SHUA) series selects examples from the daily stream of vulnerabilities in common software, which are often due to the convolution of human error and programmer-biased language design. The theme is to demonstrate with salient examples how Ada can innately protect applications from common errors.
Our first vulnerability looks at the (in)famous "Goto fail" iOS SSL/TLS vulnerability from 2014. Here is an excellent blog-post discussing the vulnerability in detail.
We'll do a really quick and simple run-down of the key points. Following is an abbreviated selection of the original code before it was patched (full listing here).
static OSStatus
SSLVerifySignedServerKeyExchange(SSLContext *ctx, bool isRsa, SSLBuffer signedParams,
uint8_t *signature, UInt16 signatureLen)
{
OSStatus err;
if ((err = ReadyHash(&SSLHashSHA1, &hashCtx)) != 0)
goto fail;
if ((err = SSLHashSHA1.update(&hashCtx, &clientRandom)) != 0)
goto fail;
if ((err = SSLHashSHA1.update(&hashCtx, &serverRandom)) != 0)
goto fail;
if ((err = SSLHashSHA1.update(&hashCtx, &signedParams)) != 0)
goto fail;
goto fail;
if ((err = SSLHashSHA1.final(&hashCtx, &hashOut)) != 0)
goto fail;
fail:
SSLFreeBuffer(&signedHashes);
SSLFreeBuffer(&hashCtx);
return err;
}
The above function's role is to verify a key exchange, returning a status code ("OSStatus") declaring the result of the verification. We see that "err" is used as a running result from a string of hash operations. The idea being that if one of the operations should fail, then that specific failure code is dutifully returned. Unfortunately this means that as long as "clientRandom", "serverRandom", and "signedParams" are successfully hashed, no actual comparison or verification is made thereafter, since the fifth goto statement is unconditionally executed, which then reports that the verification is "OK", even if it really isn't.
Now looking at this error, it is probably safe to assume that the programmer did not intentionally insert "goto fail" twice. Some speculate it came from tripping-over-keys in Vim, though most agree it was a poorly executed merge or copy-paste operation. Indeed, there are not many other conclusions to be made if deliberate actions are ruled-out.
Let's start-off by imagining what the pre-bug condition would look like in Ada. The goal here is to put ourselves in the shoes of the original programmer, and try to represent their style, as if they were an Ada programmer at the time (not necessarily a good Ada programmer).
function SSL_Versify_Signed_Server_Key_Exchange
(Context : in out SSL_Context;
Is_RSA : in Boolean;
Signed_Params: in SSL_Buffer_Access;
Signature : in SSL_Signature)
-- Note we can get "signatureLen" from Signature'Length
return OS_Status
is
Ret_Error: OS_Status;
Hash_Ctx : SSL_Buffer_Access := null;
Hash_Out : SSL_Buffer_Access := null;
Ret_Error := Ready_Hash (SSL_Hash_SHA1, Hash_Ctx);
if Ret_Error /= OK then
goto Fail;
end if;
Ret_Error := SSL_Hash_SHA1.Update (Hash_Ctx, Server_Random);
if Ret_Error /= OK then
goto Fail;
end if;
Ret_Error := SSL_Hash_SHA1.Update (Hash_Ctx, Client_Random);
if Ret_Error /= OK then
goto Fail;
end if;
Ret_Error := SSL_Hash_SHA1.Update (Hash_Ctx, Signed_Params);
if Ret_Error /= OK then
goto Fail;
end if;
Ret_Error := SSL_Hash_SHA1.Final (Hash_Ctx, Hash_Out);
if Ret_Error /= OK then
goto Fail;
end if;
<<Fail>>
SSL_Free_Buffer (Hashes);
SSL_Free_Buffer (Signed_Hashes);
SSL_Free_Buffer (Hash_Ctx);
return Ret_Error;
end SSL_Versify_Signed_Server_Key_Exchange;
One popular shortcut missing from Ada is the ability to test the result of a function simultaneously with the assignment of that function's result to a variable. We see this here, with distinct (and yes, verbose) try and test blocks for each hash operation. Like nearly everything in Ada, this is deliberate. Separating assignment from evaluation like this aids readability, and prevents unintentional side-effects.
We are not trying to make this post about improving the flawed code, or improving coding practices in general. Rather the point is to demonstrate Ada's innate ability to protect against poor practices. It is easy to say that something should be done in some way (in theory). It is a whole other thing to ensure that people will really do it (in practice). Ada was deliberately designed with the awareness that human programmers can be expected to make mistakes, and lots of them. Therefore we are not talking about how Ada enables better software engineering practices, though it certainly does. Rather, we want to demonstrate how the exact same poor practices that led to a serious vulnerability, if implemented through Ada, would have been outright precluded, or otherwise identified early-on.
Let's now simulate the most likely scenarios discussed above which could have lead to the Goto fail vulnerability appearing. We'll start with a common copy-paste replace operation.
Imagine we copy this highlighted region:
if ((err = SSLHashSHA1.update(&hashCtx, &serverRandom)) != 0)
goto fail;
And then paste it over a target region:
if ((err = SomeOtherFunction) != 0)
goto fail;
if ((err = SSLHashSHA1.final(&hashCtx, &hashOut)) != 0)
goto fail;
This is gives us the vulnerability immediately:
if ((err = SSLHashSHA1.update(&hashCtx, &serverRandom)) != 0)
goto fail;
goto fail;
if ((err = SSLHashSHA1.final(&hashCtx, &hashOut)) != 0)
goto fail;
Can we make the same error in Ada? Surely, but it could never work if the target was only a single line. We'd just end-up repeating the test of Ret_Error twice (harmlessly). So let's try to be more realistic, let's say we forgot to select the last line of the target, which is a realistic error.
So we copy the full block:
Ret_Error := SSL_Hash_SHA1.Update (Hash_Ctx, Server_Random);
if Ret_Error /= OK then
goto Fail;
end if;
Pasting over the highlighted block (minus one line - by accident):
Ret_Error := Some_Other_Function;
if Ret_Error /= OK then
goto Fail;
end if;
Ret_Error := SSL_Hash_SHA1.Final (Hash_Ctx, Hash_Out);
if Ret_Error /= OK then
goto Fail;
end if;
And we get... Something that is not valid Ada, and will be outright refused by the compiler:
Ret_Error := SSL_Hash_SHA1.Update (Hash_Ctx, Server_Random);
if Ret_Error /= OK then
goto Fail;
end if;
end if;
Ret_Error := SSL_Hash_SHA1.Final (Hash_Ctx, Hash_Out);
if Ret_Error /= OK then
goto Fail;
end if;
Of course, this scenario is caught in C too if brackets are enforced. In Ada, "end if" isn't optional. All blocks of every kind must have an "end". This is an important distinction. If this scenario is really what introduced the vulnerability, Ada would have caught it by it's very nature.
How about single line deletion? Imagine we had some other property that we no longer wanted to include in the hash. We know that would lead to the vulnerability in C. But in Ada, it is totally benign. Like with a single line replace as above, this would just result in a duplicate test of Ret_Error.
Ret_Error := SSL_Hash_SHA1.Update (Hash_Ctx, Client_Random);
if Ret_Error /= OK then
goto Fail;
end if;
if Ret_Error /= OK then
goto Fail;
end if;
Ret_Error := SSL_Hash_SHA1.Final (Hash_Ctx, Hash_Out);
if Ret_Error /= OK then
goto Fail;
end if;
In fact, overall we find that there would never be a time that Goto fail would appear outside of some kind of block, usually an if statement. Unless deliberate, it would be extremely unlikely to find the goto outside of a conditional block by sheer accident.
Even in the very worst case, where the result was programmatically identical to the original ,the default gcc compiler configuration warns us:
Ret_Error := Ready_Hash (SSL_Hash_SHA1, Hash_Ctx);
if Ret_Error /= OK then
goto Fail;
end if;
Ret_Error := SSL_Hash_SHA1.Update (Hash_Ctx, Server_Random);
if Ret_Error /= OK then
goto Fail;
end if;
Ret_Error := SSL_Hash_SHA1.Update (Hash_Ctx, Client_Random);
if Ret_Error /= OK then
goto Fail;
end if;
Ret_Error := SSL_Hash_SHA1.Update (Hash_Ctx, Signed_Params);
if Ret_Error /= OK then
goto Fail;
end if;
goto Fail;
Ret_Error := SSL_Hash_SHA1.Final (Hash_Ctx, Hash_Out);
if Ret_Error /= OK then
goto Fail;
end if;
$ gcc -c fail.adb
fail.adb:22:04: warning: unreachable code
Testing and quality standards are always basic requirements for any engineering project. However, total coverage is often impossible or impractically expensive. This is especially true for commercial software, which is not regulated in any meaningful way, unlike safety-critical software. Rather than trying to eliminate these kinds of basic errors through endlessly stricter standards and expanded testing on a more error-prone language, Ada can be leveraged to create a more focused, efficient, and reliable testing environment. In essence, using Ada introduces built-in static and dynamic analysis by design, which can eliminate or identify most common vulnerabilities, allowing testing to focus on errors in the higher-level program behavior.