The function of software used to be calculation; mechanising what was previously done by hand. Now it runs our communication networks, mass transportation and medical support. Yet we still build large software systems as if they were small, easily comprehensible tools.The right to manage our safety and security should not be handed over lightly. When a program has the ability to compromise our security or injure us, we should demand evidence of its correctness. Formal software verification has demonstrated how to reliably and repeatedly build safe and secure high-assurance systems, to a standard not achievable using other techniques. Yet it remains underused due to perceptions that it is expensive and time intensive to apply.In this thesis we demonstrate how to scale formal software verification beyond its current limits using component-based software engineering. By leveraging the strong isolation boundaries made possible by the CAmkES component platform operating on the seL4 microkernel, we decompose system verification along lines that correspond to the system architecture. The parallels between proof obligations and system architecture aid the designer’s intuition and allow easing verification challenges through architectural refactoring.To uphold the engineering abstraction that a component platform provides, we demonstrate a fully automated process for verifying functional correctness of platform-generated code and the correct initialisation of a CAmkES system. The system designer no longer needs to trust that the platform’s mechanisms do what they claim, as is the case with other existing component platforms. We also fully automate the production of an access control policy for a component-based system, allowing the designer to move seamlessly from architecture layout to security analysis, with knowledge that our verification guarantees a faithful translation.The techniques in this thesis represent novel contributions to the fields of component-based software and formal verification. To our knowledge, they provide the most trustworthy development environment for high-assurance, componentised software systems in existence today. By extending the power and scope of formal verification, we lower the cost of its application and enable the development of safer and more secure software.
展开▼
