There is value in being able to verify that the security claims made for a piece of software also actually hold. In projects with the automotive industry (Volvo Cars) and in the financial sector, we have seen techniques and tools to support a software certification process by testing that the actual software fullfils functional and security requirements. The key idea here is to have the software developers specify (security) requirements of their software in a high level programming language. The requirements must be precise, thus it should not allow room for natural language ambiguities. Property-based testing tools, invented at Chalmers University, can then be used to automatically create and run test cases to verify that these requirements hold.
Thousands of generated tests explore corner cases that may have slipped attention when writing tests by hand. I traditional testing, one can only show that “no error” is found. However, for security requirements, one would also like to establish that a system can always return to a stable state or make progress. Typical examples it showing that a piece of software cannot deadlock or will eventually recover from a denial of service attack. Recent extension to property-based testing allow formulating a strategy that, no matter which state the software is in, it can progress to a good state. With that described strategy, the automatic test case generation now brings the system in any arbitrary state and then applies the strategy to verify that indeed one can recover to a good state. Property-based testing tools are available open source. They have been applied in many areas, ranging from telecommunication, automative, video and chat servers, to blockchain and health-care applications.
The techniques can offer a part in the puzzle of acquiring trust in the actual software produced and delivered and the high degree of automation makes it possible to do this cost effective. In addition to being applied on large software projects, most of these ideas are published in scientific publications.
thomas-artsExplore the conference agenda
Sponsors
