Warning: Code Can Be Explosive

Source: U.S. Naval Historical Center Online Library Photograph NH 96566-KN
© 2006 Doug Kerr under CC BY-SA 2.0

When Tests Fail

© 2014 Emmelie Callewaert under CC BY-SA 4.0
function getWaterAmount(int last_temperature, int temperature, int last_amount): [int] {
int amount = min(0, last_amount + (temperature - last_temperature) * WATER_CONSTANT);
return [amount / n, …, amount / n];
}
function test_temperature(): bool {
int temp = getAverageTemperature(
getWaterAmount(fuzz_last_temp, fuzz_temp, min(fuzz_last_amount, 0))
);
return LOW <= temp <= HIGH;
}
  1. Do I really cover all important inputs? (see Need for Formal Verification next)
  2. Should I consult other experts on my approach? (see Audits below)

Need for Formal Verification

Functional Correctness

Specifications

Verification

int main(void) {
int x = 0;
return (x = 1) + (x = 2);
}
function foo(int n) {
// n : int
if (n > 0) { // n : int && n > 0
if (n <= 0) { // n : int && n > 0 && n <= 0
bug1();
}
}
}

Audits

  • How did you come up with that water constant?!
  • Can you really make decisions based on local state only (last_temp)?!
  • Are you sure you want to use a linear function on an exponentially behaving system?!
  • You really want to test against an average temperature metric?! That is insane!
  • What happens when you want to pump more water than available?!
  • What happens when there is a memory overflow?!
  • How did you come to the conclusion that the water should be evenly distributed?!
  • How do you schedule the entire thing? There is a whole branch of computer science devoted to the analysis of real time systems. Timing is a huge source of bugs even in single processor scheduling.

External code reviews

  1. The auditing team discusses with you the time plan and ideas about what needs to be checked.
  2. You provide secure access to your repository.
  3. The auditing team researches all your relevant materials and studies your code.
  4. The auditing team creates an abstract model of your codebase and analyzes it.
  5. The auditors refer to a database of known security flaws and check that your code does not suffer from any of them.
  6. A report is written explaining all the findings and possible solutions. You can usually choose what goes public and what response you want to include. An example report can be found here.

Conclusion

References

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Runtime Verification

Runtime Verification

157 Followers

Runtime Verification Inc. is a technology startup providing cutting edge formal verification tools and services for aerospace, automotive, and the blockchain.