Earlier this year at TROOPERS I presented on how many tenets of the LangSec theories could be integrated into a modern SDLC through providing a framework for "verification-oriented programming". This idea revolved around the notion that "to err is human, to be caught at compile-time (or as close to it as possible) divine", and that developers are going to make mistakes, but a good SDLC should be able to catch those bugs rapidly.

One simple example I used as a way to put this into practical terms is the ordering of comparisons in C:

if (variable == CONST)

versus:

if (CONST == variable)

Now, naturally these are semantically equivalent, when implemented correctly. If a developer fails to type the second "=", the former snippet will compile successfully and execute flawed semantics whereas the latter example would result in a compile-time error.

With such programming techniques, we as developers can encode additional "intent" into the software, resulting in the compiler being better able to help us check ourselves (trust, but verify) more easily. Today I watched the excellent H2HC keynote on blind memory corruption attacks and how they can be used to bypass security. In their example, a TOCTOU vulnerability in the Linux login program allows an attack who can modify memory arbitrarily (that is without complete control of new value, such as in Rowhammer or with JTAG against encrypted DRAM) log in as 'root' without knowledge of the password.

While watching this demonstration, I noticed that the vulnerability smelled of being easily-explainable by LangSec. The vulnerable code is simplified below:

int preauth = 0;
check_for_preauth_config();
if (preauth) {
  do_some_extra_authentication_checks();
}
if (main_password_checking_routine()) {
  goto login_success;
}
if (preauth) {
  goto login_success;
}
return login_fail;

As you can see, under normal assumptions of the integrity of RAM, this code should work as expected, but due to the semantic ambiguity of the if(val) construct there is a vulnerability under a more powerful attacker model, where the preauth variable can be set to anything other than 0 in order to bypass the checks. If a Rowhammer attack is successful in flipping a single bit in that memory address, the login system can be bypassed. If instead a more rigorous semantic data model was implemented, this attack would be largely defeated:

#define PREAUTH_YES 0xdeadbeef
#define PREAUTH_NO 0x1ea7f00d

int preauth = PREAUTH_NO;
check_for_preauth_config();
if (PREAUTH_YES == preauth) {
  do_some_extra_authentication_checks();
}
if (main_password_checking_routine()) {
  goto login_success;
}
if (PREAUTH_YES == preauth) {
  goto login_success;
}
return login_fail;

In conclusion, as the attack surface has grown to encompass the composition of hardware and software, certain assumptions about the integrity of the system must be revisited. Through developing in a highly-defensive manner to ensure the maximal semantic "intent" is put into the software logic, we can mitigate classes of attacks.