Ensuring Software Security and Privacy
Software based systems have a legacy of vulnerabilities across many industries. Meeting security requirements is often problematic because the context of use is either poorly defined or has changed for the implementation. The typical approach to the development of software based systems has a cost profile heavily weighted towards the end of the project; this represents considerable project risk. There are a multitude of appropriate standards for making safe systems and not many agreed international standards for secure systems and software. The Common Criteria is one such international standard, but this does not necessarily apply, especially if the system is not for a government customer. Therefore showing that a software system is secure has its challenges.
For embedded systems, such as utilities, aerospace and automotive, there is increasing interest in ensuring that they are not only safe but secure as well. The current crop of safety related standards don’t explicitly require secure software, but for some, there is an implicit security aspect, especially at the higher levels of safety assurance. However, unless security requirements have been specifically identified, it is only possible to make a general justification for security which holds little value.
It is therefore of value to be able to make claims about the invulnerability of a software system and to understand where issues may arise. This enables the identification of further measures outside of system design to mitigate remaining vulnerabilities and to document them in a security case. Gaining the required evidence from development life cycle processes that support platform safety claims needs to be designed into all stages of the life cycle. The production of evidence should therefore drive the selection of the best development life cycle, processes and tools. The production of verification evidence through review, analysis or test to meet security requirements can therefore be costly and unresponsive, even to small changes.
The use of formal methods in secure applications has a great history and is recognised at the higher levels of the Common Criteria (EAL5-7). To date, it has been assumed that experts are required to write formal specifications by hand and then to prove the necessary properties using appropriate qualified tools as support. This is not necessarily a quick or repeatable process and where formal techniques have been used, they have become company specific knowledge, not available to the wider community. Therefore in order for formal techniques to be adopted more widely to show security requirements are met, they need to be automated in order to achieve the required flexibility, repeatability, have a low training overhead, as well as providing evidence to support the overall platform security case.
D-RisQ has taken an approach which enables the power of formal methods to be exploited without any specialist training. By using commonly available tools such as Simulink® and commercial autocoders it is now possible for current engineers to develop systems and software in a rigorous manner, whilst gaining as a by-product, the required evidence to support certification. The D-RisQ automated suite of tools includes Modelworks® and CLawZ® which tackle different aspects of verification. The tools can be qualified to support both development and verification and support an independence argument which strengthens the support to the platform safety case.
Modelworks® proves that requirements have been correctly captured in a design expressed in Stateflow®, or will show the manner in which compliance has failed. The design can be of a System of Systems, a single system or a software program. It allows a designer to check that the design does what is required. More importantly, it allows a proof that undesired properties will never happen, a check that is typically attempted at the end of a development life-cycle. It is also possible to show behaviour under failure conditions which may be characterised as a system under attack. Modelworks can be used to show the behaviour of highly distributed Systems-of Systems such as those used in finance or railway signalling and can be used to help the safe implementation of upgrades, including the behaviour of human interaction where necessary.
CLawZ® automatically proves that automatically produced code implements a design expressed in Simulink®. By using the ADI Ada auto-coder or the TargetLink® C auto-coder aligned to the Simulink control system subset, CLawZ produces evidence that the code correctly implements the design, or shows where the coder has made a mistake. This relieves the need to undertake unit testing thus gaining considerable time benefits.