Autor: Chris Hobbs, QNX Software Systems<\/p>\n
Die verschiedenen Sicherheitsnormen (ISO 26262, IEC 61508 usw.) verlangen die Erstellung eines Sicherheitsnachweises. Diverse Untersuchungen haben belegt, dass eine solche Aufgabe oft zu Best\u00e4tigungsfehlern f\u00fchrt. Diese Abhandlung beschreibt eine praktische Anwendung der eliminativen Induktion, um das Ph\u00e4nomen des Confirmation Bias positiv zu nutzen. Im Verlauf einer k\u00fcrzlich erfolgten ISO\u00a026262\/IEC\u00a061508 Zertifizierung hat dieses Vorgehen mehrere Sicherheitsl\u00fccken aufgedeckt, die bis dahin unbemerkt geblieben waren.<\/strong><\/p>\n QNX Software Systems hat seit 2010 diverse Produkte erfolgreich durch Pr\u00fcfungen gem\u00e4\u00df ISO\u00a026262, IEC\u00a061508 und IEC\u00a062304 zertifizieren lassen. F\u00fcr jede Pr\u00fcfung war von QNX ein Sicherheitsnachweis (sog. \u00bbSafety Case\u00ab) vorzubereiten. Gem\u00e4\u00df den Normen besteht ein Sicherheitsnachweis aus drei Teilen: die Behauptung (was leistet das System, und unter welchen Bedingungen), das Argument (wie best\u00e4tigen wir, dass das System sicher ist) und die Beweismittel (die das Argument unterst\u00fctzen). Damit soll die Sicherheit des Systems bewiesen werden k\u00f6nnen.<\/p>\n Wie die Referenzen [1] und [2] zeigen, ist es f\u00fcr Menschen sehr schwierig, fast unm\u00f6glich, Best\u00e4tigungsfehler (sog. \u00bbConfirmation Bias\u00ab) zu vermeiden. Wenn man die Aufgabe hat, zu beweisen, dass das System sicher ist, bemerkt man nur die Nachweise, die zeigen, dass das System sicher ist!<\/p>\n In seinem Bestseller (Referenz [5]) hat Rolf Dobelli den Confirmation Bias so beschrieben: \u00bbDer Confirmation Bias ist der Vater aller Denkfehler \u2013 die Tendenz, neue Informationen so zu interpretieren, dass sie mit unseren bestehenden Theorien, Weltanschauungen und \u00dcberzeugungen kompatibel sind. \u2026 Neue Informationen, die im Widerspruch zu unseren bestehenden Ansichten stehen \u2026 filtern wir aus. Das ist gef\u00e4hrlich.\u00ab<\/p>\n Dieser Vortrag beschreibt, wie QNX den Confirmation Bias positiv genutzt hat, um einen vertrauensw\u00fcrdigeren Sicherheitsnachweis vorzubereiten.<\/p>\n Obwohl das Falsifikationsprinzip normalerweise im Zusammenhang mit Karl Popper im 20. Jahrhundert betrachtet wird, hatte Francis Bacon es schon 1597 in seinem\u00a0Novum Organum<\/em>\u00a0vorhergesehen (Referenz [6]).<\/p>\n 2013 hat John Goodenough (et al, Referenz [4]) \u201eEliminative Induction\u201c ver\u00f6ffentlicht. Diese beschreibt, wie Bacons Ideen \u00fcber \u00bbEliminative Induction\u00ab (auch als \u00bbEliminative Argumentation\u00ab bekannt) genutzt werden k\u00f6nnen, um Sicherheitsnachweise zu verbessern. QNX hat diese Ideen w\u00e4hrend der Zertifizierung des QOS\u00a02.0-Systems getestet.<\/p>\n Die Grundidee ist einfach: Anstatt Nachweise zu suchen, die das Argument positiv best\u00e4tigen, sucht man Beispiele, die das Argument in Zweifel ziehen. Danach muss jeder dieser Zweifel ausgeschlossen werden \u2013 dadurch nutzt man die unvermeidbaren Best\u00e4tigungsfehler zum Vorteil.<\/p>\n Im Wesentlichen sagt man: \u00bbIch habe alle Zweifel an der Sicherheit meines Systems, die ich mir vorstellen kann, identifiziert. Und jetzt kann ich belegen, dass jeder dieser Zweifel unbegr\u00fcndet ist. Deshalb bin ich der Meinung, dass das System sicher ist\u00ab.<\/p>\n Tabelle 1 der ISO\u00a026262-6:2011 empfiehlt \u201cUse of Language Subsets\u201d und Tabelle C.1 der IEC\u00a061508-7:2010 empfiehlt die C-Programmiersprache gar nicht, au\u00dfer wenn \u201cC with subset and coding standard, and use of static analysis tools\u201d benutzt wird.<\/p>\n Als Beispiel (nicht aus QNX-Erfahrung genommen!) zeigt Bild 1 (s.\u00a0PDF<\/a>) einen kleinen Teil des Arguments eines Sicherheitsnachweises eines imagin\u00e4ren Produkts. Die Darstellung folgt der Goal Structuring Notation (Referenz [3]) und enth\u00e4lt nur zwei Symbole:<\/p>\n Hat man die Aufgabe, die Sicherheit des Systems zu demonstrieren, um dieses Argument zu pr\u00fcfen, braucht man nur das Dokument ABC123 zu finden, und zu verifizieren, dass es blo\u00df eine Teilmenge von C erlaubt.<\/p>\n Allerdings ist es m\u00f6glich, drei Arten von Zweifeln hervorzubringen. In Referenz [4] sind diese wie folgt genannt:<\/p>\n Bild 2 (s.\u00a0PDF<\/a>) weitet Bild 1 mit m\u00f6glichen \u201cundermining\u201d und \u201cundercutting\u201d Zweifeln aus. IR36a macht die zugrunde liegende Annahme deutlich: \u201cWenn ein Dokument existiert, das die Teilmenge definiert, so muss die Teilmenge verwendet werden\u201d. Wenn es so erl\u00e4utert wird, ist es einfach, Zweifel daran aufzuwerfen \u2013 kann man einen Programmierer finden, der dieses Dokument\u00a0nicht<\/em>\u00a0anwendet oder\u00a0nicht<\/em>\u00a0versteht (UC36a)? Man k\u00f6nnte auch einen \u201cundercutting\u201d Zweifel finden: Was enth\u00e4lt das Dokument ABC123? Die Normen verlangen nur eine Teilmenge der C-Sprache, aber es ist implizit, dass die Teilmengen n\u00fctzlich sein m\u00fcssen: es gen\u00fcgt nicht nur \u00bbGOTO darf nicht benutzt werden\u00ab zu spezifizieren. Wurde der Inhalt von Dokument ABC123 gepr\u00fcft? Von wem? War er kompetent?<\/p>\n Die Zweifel m\u00fcssen jetzt eliminiert werden. Vielleicht k\u00f6nnte man nachpr\u00fcfen, ob Dokument ABC123, das die Coding Standards definiert, von qualifizierten Menschen \u00fcberpr\u00fcft wurde. Wenn ja, sollten Berichte zur Verf\u00fcgung stehen, die die \u00dcberpr\u00fcfung beschreiben. Bild 3 (s.\u00a0PDF<\/a>) zeigt, wie diese Information einbezogen werden kann: Review Record 143521 zeigt, dass man ABC123 \u00fcberpr\u00fcft hat. Auf eine \u00e4hnliche Weise k\u00f6nnte man eine Probennahme des Codes mit einem Static-Analysis-Werkzeug durchf\u00fchren, um herauszufinden, ob die Programmierer die Vorschriften beachtet haben: AHF736.<\/p>\n Nun k\u00f6nnte man, wie kleine Kinder es tun, weiter und weiter nachbohren: \u201eAber ist es nicht auch m\u00f6glich, dass \u2026 ?\u201c Das w\u00fcrde aber zu abnehmenden Ertr\u00e4gen f\u00fchren. Nach technischem Verst\u00e4ndnis ist es nicht n\u00fctzlich, immer tiefer einzusteigen.<\/p>\n QNX hat dieses Verfahren w\u00e4hrend der Vorbereitung seines aktuellen Sicherheitsnachweises (2018) des QOS\u00a02.0 Betriebssystems angewendet. Dieses Betriebssystem war 2010 gem\u00e4\u00df IEC\u00a061508 (SIL3), 2012 gem\u00e4\u00df IEC\u00a062304 und 2015 und 2016 gem\u00e4\u00df ISO\u00a026262 (ASIL-D) und IEC\u00a061508 (SIL3) schon zertifiziert worden.<\/p>\n Um Best\u00e4tigungsfehler zu vermeiden, hatten wir damals f\u00fcr diese fr\u00fcheren Produkte zwei strukurierte, semi-formale Argumente vorbereitet: mit Goal Structuring Notation bzw. Bayessche Netzwerke Notation.<\/p>\n Obwohl diese fr\u00fcheren Sicherheitsnachweise professionell vorbereitet wurden, und obwohl man die Gefahren von Best\u00e4tigungsfehlern zwar gut begriffen hatte, hat die neuste Analyse, die mit dem hier beschriebenen Verfahren durchgef\u00fchrt wurde, etwa zwanzig Probleme gefunden, die w\u00e4hrend vorheriger Zerifizierungen nicht aufgedeckt worden waren.<\/p>\n Da sich diese neue Analyse als so erfolgreich erwiesen hat, haben wir entschieden, dass unser Bayessche-Netzwerk-Modell nicht l\u00e4nger erforderlich ist.<\/p>\n Nat\u00fcrlich haben wir uns die Frage gestellt: Warum hatten wir diese Sicherheitsprobleme nicht fr\u00fcher entdeckt? Insbesondere, warum hatte das Bayessche-Netzwerk-Modell sie nicht gefunden?<\/p>\n Um diese Frage beantworten zu k\u00f6nnen, haben wir verschiedene Programmierer befragt.<\/p>\n Als Beispiel untersuchten wir ein Problem, das sich mit Code Review besch\u00e4ftigt und durch dieses neue Verfahren entdeckt wurde. Die QNX Code-Review-\u00dcberpr\u00fcfungsvorschrift verlangt, dass die Ergebnisse der Static Analysis immer mit einem Code Review ver\u00f6ffentlicht werden m\u00fcssen. Der Programmierer soll nicht nur die vorgeschlagenen \u00c4nderungen des Codes, sondern auch von den Static-Analysis-Warnungen mit dem \u00dcberpr\u00fcfungsantrag berichten.<\/p>\n In der Vergangenheit hat der Auditor sowohl das Verfahren als auch die Pr\u00fcfung des Verfahrens kontrolliert. Er hat dazu einige Reviews \u00fcberpr\u00fcft. Dabei wurde kein einziges Problem gefunden. Auf die Frage, ob der Vorgang vollst\u00e4ndig durchgef\u00fchrt worden ist, best\u00e4tigten die Programmierer: \u00bbJa, nat\u00fcrlich folgen wir dem richtigen Verfahren\u00ab.<\/p>\n Stellten wir dir Frage umgekehrt: \u00bbKannst Du dich an Beispiele erinnern, wo die Static Analysis Warnungen nicht mit der \u00dcberpr\u00fcfungsvorschrift ver\u00f6ffentlicht wurden?\u00ab, best\u00e4tigten die gleichen Programmierer auch dies positiv. Obwohl die Warnungen beim ersten Schritt des Reviews immer gezeigt werden, wurden sie jedoch gelegentlich weggelassen, wenn der Code w\u00e4hrend sp\u00e4terer Schritte ver\u00e4ndert werden musste.<\/p>\n QNX hat die Richtlinien von Referenz [4] erweitert und genutzt, um einen Sicherheitsnachweis vorzubereiten.<\/p>\n Dieser Nachweis hat die Zertifizierung des Betriebssystems gem\u00e4\u00df ISO\u00a026262 (ASIL-D) und IEC\u00a061508 (SIL3) von T\u00dcV Rheinland unterst\u00fctzt. Au\u00dferdem hat dieses neue Verfahren auch diverse sicherheitsrelevante Probleme gefunden, die w\u00e4hrend vorheriger Zertifizierungen nicht aufgedeckt wurden. Diese konnten wir dann vor der Produktfreigabe eliminieren.<\/p>\n QNX hat diese Ergebnisse mit der \u00bbAssurance Case Working Group\u00ab (https:\/\/scsc.uk\/gc<\/a>) geteilt.<\/p>\n [1] „Die Bayessche Darstellung eines Sicherheitsnachweises“, Chris Hobbs, Embedded Systems Engineering Kongress, Sindelfingen, Dezember 2015<\/p>\n [2] „White Paper on the Use of Safety Cases in Certification and Regulation“, Nancy Leveson, 2012<\/p>\n [3] „GSN COMMUNITY STANDARD VERSION 1“, November 2011.<\/p>\n [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<\/p>\n [5] „Die Kunst des Klaren Denkens“, Rolf Dobelli, 2014, ISBN 978-3-423-34826-3<\/p>\n [6] \u201cNovum Organum Scientiarum\u201d, Francis Bacon, 1620, https:\/\/www.thelatinlibrary.com\/bacon.html<\/p>\n Chris ist Programmierer bei QNX Software Systems. Sein Spezialgebiet ist „ausreichend verf\u00fcgbare“ Software: Software, in die mindestens so viel Entwicklungsaufwand gesteckt wurde, dass sie den Anspr\u00fcchen bez\u00fcglich Ausfallsicherheit und Zuverl\u00e4ssigkeit des Kunden gerecht wird. Au\u00dferdem befasst er sich mit Sicherer Software (Konformit\u00e4t mit IEC\u00a061508, ISO\u00a026262 und IEC\u00a062304). Neben seiner Arbeit im Bereich Software-Entwicklung ist Chris Hobbs au\u00dferdem als Fluglehrer t\u00e4tig, singt gerne (vor allem Schubertlieder) und ist Autor einiger weiterer B\u00fccher, z.B.\u00a0Flying Beyond: The Canadian Commercial Pilot Textbook\u00a0<\/em>und\u00a0Embedded Software Development for Safety-Critical Systems<\/em>.<\/p>\n Beitrag als PDF downloaden<\/strong><\/a><\/p>\n Wollen Sie sich auf den aktuellen Stand der Technik bringen?<\/strong><\/p>\n Dann informieren Sie sich\u00a0hier<\/strong>\u00a0<\/a>zu Schulungen\/ Seminaren\/ Trainings\/ Workshops und individuellen Coachings von MircoConsult zum Thema\u00a0Qualit\u00e4t, Safety & Security<\/strong>.<\/p>\n Training & Coaching zu den weiteren Themen unseren Portfolios finden Sie hier<\/a>.<\/strong><\/p>\n Wertvolles Fachwissen zum Thema Qualit\u00e4t, Safety & Security steht\u00a0hier\u00a0<\/a><\/strong>f\u00fcr Sie zum kostenfreien Download bereit.<\/p>\nEinf\u00fchrung<\/h2>\n
Das Falsifikationsprinzip<\/h2>\n
Ein Beispiel<\/h3>\n
\n
\n
Die Ergebnisse<\/h2>\n
Erl\u00e4uterung<\/h2>\n
Zusammenfassung<\/h2>\n
Literatur<\/h2>\n
Autor<\/h2>\n
\nUnsere Trainings & Coachings<\/h2>\n
\nQualit\u00e4t, Safety & Security – Fachwissen<\/h2>\n