Select Page

Improving safety verification through induction

Can a concept from the 16th century be useful?

Author: Chris Hobbs, QNX Software Systems

Contribution – Embedded Software Engineering Congress 2018

Various safety standards (ISO 26262, IEC 61508, etc.) require the creation of a safety verification. Numerous studies have shown that such a task often leads to confirmation bias. This paper describes a practical application of eliminative induction to leverage the phenomenon of confirmation bias. During a recent ISO 26262/IEC 61508 certification, this approach uncovered several previously undetected security vulnerabilities.

introduction

Since 2010, QNX Software Systems has successfully certified various products through testing according to ISO 26262, IEC 61508, and IEC 62304. For each certification, QNX was required to prepare a safety case. According to the standards, a safety case consists of three parts: the claim (what the system does and under what conditions), the argument (how we confirm that the system is safe), and the evidence (which supports the argument). This is intended to demonstrate the system's safety.

As references [1] and [2] show, it is very difficult, almost impossible, for humans to avoid confirmation bias. When tasked with proving that a system is secure, one only notices the evidence that already shows the system is secure!

In his bestseller (reference [5]), Rolf Dobelli described confirmation bias as follows: »Confirmation bias is the father of all cognitive errors – the tendency to interpret new information in a way that is compatible with our existing theories, worldviews, and beliefs. … We filter out new information that contradicts our existing views. … This is dangerous.«

This presentation describes how QNX has used confirmation bias to its advantage in order to prepare a more trustworthy proof of security.

The falsification principle

Although the falsification principle is usually considered in connection with Karl Popper in the 20th century, Francis Bacon had already described it in 1597 in his Novum Organum predicted (reference [6]).

In 2013, John Goodenough (et al, reference [4]) published "Eliminative Induction." This describes how Bacon's ideas on "Eliminative Induction" (also known as "Eliminative Argumentation") can be used to improve safety evidence. QNX tested these ideas during the certification of the QOS 2.0 system.

The basic idea is simple: Instead of looking for evidence that positively confirms the argument, one looks for examples that cast doubt on the argument. Then, each of these doubts must be eliminated – thereby turning the unavoidable confirmation bias to one's advantage.

Essentially, one is saying: "I have identified every conceivable doubt about the security of my system. And now I can prove that every one of these doubts is unfounded. Therefore, I believe that the system is secure.".

An example

Table 1 of ISO 26262-6:2011 recommends “Use of Language Subsets” and Table C.1 of IEC 61508-7:2010 does not recommend the C programming language at all, except when “C with subset and coding standard, and use of static analysis tools” is used.

As an example (not taken from QNX experience!), Figure 1 (see below) shows... PDF) a small part of the argument for a safety proof of an imaginary product. The representation follows the Goal Structuring Notation (reference [3]) and contains only two symbols:

  1. A “Goal” (G36). This states that the programmers used only a subset of C during product development, in accordance with the standards.
  2. A “solution” (Sn36). The evidence supporting G36 is the document ABC123. This document presumably contains the coding standard that defines the subset.

If the task is to demonstrate the security of the system in order to test this argument, one only needs to find the document ABC123 and verify that it allows only a subset of C.

However, it is possible to raise three types of doubt. In reference [4], these are listed as follows:

  1. Rebutting (refuting). Can counterexamples be found?
  2. Undermining (corrosive). Could the evidence be invalid?
  3. Undercutting. Does the evidence fail to support the claim? Perhaps the evidence is true, but irrelevant nonetheless.

Image 2 (see. PDFFigure 1 expands upon possible “undermining” and “undercutting” doubts. IR36a clarifies the underlying assumption: “If a document exists that defines the subset, then the subset must be used.” When explained in this way, it is easy to raise doubts – can one find a programmer who uses this document? not applies or not Does it understand (UC36a)? One could also find an undercutting doubt: What does document ABC123 contain? The standards only require a subset of the C language, but it is implicit that the subsets must be useful: it is not enough to simply specify "GOTO must not be used". Was the content of document ABC123 reviewed? By whom? Was the reviewer competent?

These doubts must now be eliminated. Perhaps it could be verified whether document ABC123, which defines the coding standards, was reviewed by qualified individuals. If so, reports describing the review should be available. Figure 3 (see below). PDF) shows how this information can be incorporated: Review Record 143521 shows that ABC123 has been reviewed. Similarly, one could perform a code sampling with a static analysis tool to determine whether the programmers have complied with the regulations: AHF736.

One could, like small children do, keep probing: "But isn't it also possible that...?" However, this would lead to diminishing returns. From a technical perspective, it's not useful to keep digging deeper.

The results

QNX applied this procedure during the preparation of its current safety certification (2018) for the QOS 2.0 operating system. This operating system had already been certified in 2010 according to IEC 61508 (SIL3), in 2012 according to IEC 62304, and in 2015 and 2016 according to ISO 26262 (ASIL-D) and IEC 61508 (SIL3).

To avoid confirmation errors, we had prepared two structured, semi-formal arguments for these earlier products: using Goal Structuring Notation and Bayesian Network Notation, respectively.

Although these previous safety assessments were professionally prepared, and although the dangers of confirmation errors were well understood, the latest analysis, carried out using the procedure described here, found about twenty problems that had not been detected during previous certifications.

Since this new analysis has proven so successful, we have decided that our Bayesian network model is no longer needed.

Explanation

Naturally, we asked ourselves: Why hadn't we discovered these security problems earlier? In particular, why hadn't the Bayesian network model found them?

To answer this question, we interviewed various programmers.

As an example, we examined a problem related to code review that was discovered using this new procedure. The QNX code review policy requires that the results of static analysis must always be published with a code review. The programmer is expected to report not only the proposed code changes but also the static analysis warnings in the review request.

In the past, the auditor has reviewed both the process and the auditing of the process. He has examined several reviews and found no problems whatsoever. When asked whether the process had been carried out completely, the programmers confirmed: "Yes, of course we are following the correct procedure.".

When we asked them the reverse question: "Can you recall any examples where the Static Analysis warnings were not published with the review protocol?", the same programmers confirmed this as well. Although the warnings are always shown in the first step of the review, they were occasionally omitted if the code had to be changed during later steps.

Summary

QNX has extended and used the guidelines of Reference [4] to prepare a safety evidence.

This verification supported the certification of the operating system according to ISO 26262 (ASIL-D) and IEC 61508 (SIL3) by TÜV Rheinland. Furthermore, this new procedure also identified several safety-related issues that had not been detected during previous certifications. We were then able to eliminate these before product release.

QNX has discussed these results with the »Assurance Case Working Group« (https://scsc.uk/gc) shared.

literature

[1] „The Bayesian Presentation of a Safety Proof“, Chris Hobbs, Embedded Systems Engineering Congress, Sindelfingen, December 2015

[2] „White Paper on the Use of Safety Cases in Certification and Regulation“, Nancy Leveson, 2012

[3] „GSN COMMUNITY STANDARD VERSION 1,“ November 2011.

[4] „Eliminative Induction: A Basis for Arguing System Confidence,“ John B Goodenough, Charles B Weinstock and Ari Z Klein, New Ideas and Emerging Results Workshop, International Conference on Software Engineering, 2013

[5] „The Art of Clear Thinking“, Rolf Dobelli, 2014, ISBN 978-3-423-34826-3

[6] “Novum Organum Scientiarum”, Francis Bacon, 1620, https://www.thelatinlibrary.com/bacon.html

author

Chris is a programmer at QNX Software Systems. His specialty is "sufficiently available" software: software into which at least enough development effort has been invested to meet the customer's requirements for fault tolerance and reliability. He also deals with secure software (compliance with IEC 61508, ISO 26262, and IEC 62304). Besides his work in software development, Chris Hobbs is also a flight instructor, enjoys singing (especially Schubert songs), and is the author of several other books, e.g. Flying Beyond: The Canadian Commercial Pilot Textbook and Embedded Software Development for Safety-Critical Systems.

Download the article as a PDF


Our training courses & coaching sessions

Do you want to bring yourself up to date with the latest technology?

Then find out more here Regarding training courses/seminars/workshops and individual coaching sessions offered by MircoConsult on the topic Quality, Safety & Security.

Training & coaching on the other topics in our portfolio can be found here. here.


Quality, Safety & Security – Expertise

Valuable expertise on the topics of quality, safety & security is available. here Available for you to download free of charge.

To the specialist information

You can find expertise on other topics in our portfolio here. here.

MicroConsult Newsletter

With the MicroConsult newsletter, you'll stay on the pulse of the embedded world. Look forward to proven practical knowledge, real professional tips, and current events – directly from our experts for your project success.

Subscribe now!

Published by

weissblau media

weissblau media