Case study Certibus
As security assurance and certification of software remain complex, time-consuming and often fragmented, fortiss has developed a systematic, knowledge-model-based workflow. The solution integrates formal methods, domain knowledge and tools for assurance into a framework for continuous security assurance. The result: a scalable and explainable certification process, validated on a real, multi-component UAV (Unmanned Aerial Vehicle) platform.
The ARCOS programme (Automated Rapid Certification Of Software) of the Defence Advanced Research Projects Agency (DARPA) supports cutting-edge research into the automation and acceleration of software certification. The DesCert consortium, led by SRI International in close collaboration with fortiss, aimed to develop evidence-based certification schemes for newly developed, safety-critical software systems – for example in the field of autonomous aerospace.
Challenge
Traditional software certification processes – particularly in security and safety-critical domains – are slow, expensive and labour-intensive. They scale poorly with the increasing complexity of modern software and struggle to keep pace with its continuous evolution. DARPA therefore required a workflow that would enable the generation, organisation and maintenance of reliable evidence of system assurance (assurance evidence) throughout the entire lifecycle of a system.
Solution
fortiss developed a method for verifying system properties based on structured knowledge models and integrated into a pipeline for the ongoing generation of evidence. Existing models for safety-critical knowledge were extended to cover security aspects as well – including the linking of vulnerabilities, threats and countermeasures. Using tools such as Radler (architecture modelling), CLEAR (requirements) and the Checker Framework (static code analysis), workflows were formalised and linked to a central knowledge base (RACK).
In addition, fortiss developed the Evidential Tool Bus (ETB2) software for the continuous synchronisation of evidence across different tools – ensuring full traceability and verifiability.
Result
- Extension of safety assurance methods to include cybersecurity aspects through structured, formal knowledge models
- Enabling continuous certification via ETB2, which automatically collects, synchronises and keeps evidence up to date
- Integration of 12 analysis tools and over 50 evidence requirements into a single semantic model
- Automated transfer of evidence into RACK significantly reduces the manual effort involved in building security evidence
- Development of a model with 8 influencing factors for describing and analysing system interactions in cyber-physical systems
- Development of knowledge models on attackers, threats, vulnerabilities and protective measures for systematic security analyses
- Use of graph-based analyses for the automatic detection of previously unconsidered attack paths
- Mapping of real-time system interactions using Radler, ROS2 and DDS, including evidence for the isolation of individual components
- Practical validation of the entire architecture on a real UAV platform under realistic attack scenarios
- Implementation of ETB2 to control and coordinate the continuous verification workflow
- Introduction of an analysis to monitor and limit security-critical data flows within the system
- Use of CLEAR and Text2Test for the formal description of evidence and its linking to structured evidence
Outcome
The knowledge-model-based assurance methodology developed demonstrates that continuous security verification for complex cyber-physical systems can be implemented in a scalable and traceable manner through the close integration of formal methods, domain knowledge and automated tool workflows. This makes it clear that security and certifiability must be embedded in the system design from the outset in order to enable efficient, reusable and evidence-driven verification processes throughout the entire software lifecycle.
Project partner
