Evidentia

Evidentia

A framework for continuous and accountable software certification

Evidentia

The complexity of embedded software and increasing demands on safety has already outpaced the capabilities of current verification and certification methods. The Evidentia framework provides container-based services that automatically and continuously execute verification workflows in a decentralized manner to generate formal safety arguments supported by accountable evidence that corroborate safety of the software.

Project description

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 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 artefacts for software with learning enabled components.

Project contribution

Evidentia is built on the following three corner stones:

Formal Arguments: Evidentia 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.

DistributedAccountability: Distributed Ledger Technology ensures accountability of transactions by logging evidential transactions. This means that it is possible for certification auditors to infer from the log which party is responsible for evidences and which parts of safety arguments.

Funding

Internal and through different projects

Project duration

Ongoing

Dr. Tewodros Beyene

Your contact

Dr. Tewodros Beyene

+49 89 3603522 24
beyene@fortiss.org

More information

Project partner

SRI International

Publications

  • 2018Evidential and Continuous Integration of Software Verification ToolsTewodros Beyene and Harald Rueß In Formal Methods, pages 679-685, Cham, Springer International Publishing. DetailsBIB