A framework for continuous and accountable software certification
The project is aimed at devising techniques for establishing safety claims for a given software by means of decentralized arguments and supporting evidence. On one hand, the project develops formal and semi-formal languages for specifying safety argumentation patterns that can be found in certification standards and guidelines as well as good industrial practices. The languages should also be expressive enough to describe resulting safety claims and arguments.
On the other hand, the project develops algorithms for the decentralized execution of safety arguments where multiple entities will collaborate to establish a given claim. It is important to devise a secure way of exchanging claims and supporting evidence between interacting entities. Finally, the project gives special focus to emerging applications of AI by developing safety argumentation patterns and sufficient evidence artifacts for software with learning-enabled components.
ETB2 is built on the following three corner stones:
Formal Arguments: ETB2 formalizes the policies used in safety arguments as logical specifications in Cyberlogic, a first-order attestation logic for evidential transactions. These policies are programed in the form of distributed logic programs. These specifications combine logical inference with evidences generated by verification workflows. This means that safety arguments used in safety cases have precise semantics, thus enabling certification assessment to be carried out incrementally and continuously in an automated fashion.
Workflows as Services: Automated software verification workflows, specified in Cyberlogic, enable the automated generation of evidence by executing existing state-of-the-art software verification tools. Services are decentralized, container-based components that provide such verification workflows, thus supporting scalability in operational environments.
Internal and through different projects
Ongoing
