Wie verbessert formale Verifikation die Sicherheit von Embedded-Software? Mathematisch fundierte Fehlerfreiheit und hohe Code-Zuverlässigkeit sind essenziell.(Bild: Augusto - stock.adobe.com)
Fehlerfreiheit ist kein Versprechen, sondern ein Nachweis. Formale Verifikation ermöglicht mathematisch überprüfbare Software-Zuverlässigkeit – ein entscheidender Schritt für sichere Embedded-Systeme in hochkritischen Anwendungen.
Anzeige
Embedded-Software ist nicht nur einTeil unserer Welt, sie istunsere Welt. Sie findet sich in Fahrzeugen, in der Luft-/Raumfahrttechnik, in medizintechnischen Geräten, in der industriellen Automatisierung – praktisch überall dort, wo Zuverlässigkeit und Sicherheit an erster Stelle stehen.
Die Herausforderungen sind klar. Wir schaffen die Grundlage für den Betrieb kritischer Systeme und brauchen Lösungen, die über herkömmliche Testmethoden hinausgehen und mathematisch nachgewiesene Garantien für Korrektheit bieten. Damit einher geht die Forderung nach deterministischen Garantien für die Abwesenheit von Laufzeitfehlern im Code und nach Tools, die mit der Komplexität des Codes skalieren können und nicht gegen sie.
Anzeige
Digitaler Thementag: Edge-KI in der Praxis
Lokale KI-Modelle ermöglichen Echtzeitanalyse und Anomalieerkennung direkt am Sensor – ohne Umweg über die Cloud. In zwei technischen Deep-Dives erfahren Sie, wie Predictive-Maintenance-Systeme durch kontinuierliches Lernen robuster werden und wie sich KI-Modelle mithilfe von Techniken wie Taylor-Pruning und Quantisierung effizient für Embedded-Hardware anpassen lassen.
Mit Beiträgen von:
Christoph Stockhammer, Principal Application Engineer, The MathWorks GmbH
Elias Kettunen, Development Engineer, Cicor Management AG
Nutzen Sie die Gelegenheit, sich mit Experten aus der Industrie, Forschung und Entwicklung zu vernetzen und auszutauschen.
Die Entwicklung robuster Embedded-Software ist keine einfache Aufgabe, sondern mit mehreren zentralen Herausforderungen verbunden:
Sicherheitskritische Anforderungen: Die Folgen eines Ausfalls können von finanziellen Verlusten bis hin zu Verletzungen oder sogar Todesfällen reichen. Dies erfordert strenge Verifikationsprozesse, um sicherzustellen, dass die Software unter allen Umständen wie vorgesehen funktioniert.
Sicherheitsbedrohungen: Von Fahrzeug-ECUs bis hin zu IoT-Geräten können Schwachstellen in Embedded-Software ausgenutzt werden, um ganze Systeme zu kompromittieren. Der Schutz vor diesen Bedrohungen erfordert robuste Sicherheitsmaßnahmen während des gesamten Entwicklungszyklus.
Ressourcenbeschränkungen: Embedded-Systeme arbeiten oft mit begrenzter Rechenleistung, Speicherkapazität und Energie. Dies erschwert das Einbinden komplexer Sicherheitsfunktionen und Verifizierungstechniken. Entwickler müssen Wege finden, den Code hinsichtlich der Leistungsfähigkeit als auch der Sicherheit zu optimieren.
Strenge Compliance: Die Fahrzeugbranche folgt beispielsweise der Norm ISO 26262, während die Luft-/Raumfahrtindustrie die Norm DO-178C befolgt. Die Einhaltung dieser Standards erfordert ein tiefes Verständnis der Anforderungen und die Fähigkeit, die Konformität durch strenge Tests und Verifikationen nachzuweisen.
Hohe Fehlerkosten: Das Auffinden und Beheben von Fehlern in Embedded-Software nach der Veröffentlichung kann teuer und zeitaufwändig sein. Oft müssen Produkte zurückgerufen, Sicherheitspatches herausgegeben und möglicherweise rechtliche Verpflichtungen erfüllt werden. Um diese Kosten zu minimieren, ist eine frühzeitige Fehlererkennung entscheidend.
Anzeige
Sicherheitskritische Anwendungen wie Fahrzeuge sind auf robuste Embedded-Software angewiesen. Die Folgen eines Ausfalls können schnell Leben gefährden.(Bild: city of pictures - stock.adobe.com)
Bei der formalen Verifizierung werden mathematische Techniken eingesetzt, um das Systemverhalten rigoros zu analysieren. Im Gegensatz zu herkömmlichen Testmethoden, die nur das Vorhandensein von Fehlern nachweisen können, zielt die formale Verifikation von Software darauf ab, die Abwesenheit von Fehlern nachzuweisen. Das bedeutet, dass die Software exakt wie spezifiziert funktioniert und mathematisch bewiesen ist.
Die entscheidenden Vorteile der formalen Verifikation
Anzeige
Die formale Verifikation bietet gegenüber herkömmlichen Testmethoden mehrere überzeugende Vorteile:
Risikominderung: Durch die Beseitigung von Laufzeitfehlern und Schwachstellen reduziert die formale Verifikation die Wahrscheinlichkeit von Softwareausfällen erheblich.
Kosteneffizienz: Die formale Verifikation erfordert zwar eine Vorabinvestition, kann aber langfristig erhebliche Kosten einsparen. Durch das frühzeitige Erkennen und Beheben von Fehlern im Entwicklungszyklus werden Nacharbeiten minimiert und das Risiko kostspieliger Rückrufe oder Sicherheitsverletzungen reduziert.
Compliance-Sicherung: Viele Branchenstandards, wie ISO 26262 und DO-178C, schreiben eine formale Verifizierung für sicherheitskritische Software vor. Durch den Einsatz formaler Verifikation lässt sich der Compliance-Prozess optimieren.
Garantierte Speichersicherheit: Die Bedeutung liegt im Nachweis der Abwesenheit von Speicherschwachstellen. Dies ist entscheidend, um Sicherheitsverletzungen zu vermeiden und die Stabilität von Embedded-Systemen zu gewährleisten.
Das Herzstück der Lösungen von TrustInSoft ist TrustInSoft Analyzer, ein aktuelles Code-Analyse-Tool, das die Leistungsfähigkeit der formalen Verifizierung nutzt, um Code-Analysefunktionen zu bieten.
Anzeige
Mit dem TrustInSoft Analyzer lässt sich die Korrektheit des Codes nachweisen, indem Tests verifiziert und alle möglichen Ausführungspfade untersucht werden und sogar ein formaler Nachweis für den kritischsten Code erbracht wird. Was das Tool noch weiter auszeichnet, ist die Möglichkeit, das Endergebnis ohne Hardware zu simulieren. Diese hardwarebewusste Analyse hilft, den Entwicklungszyklus zu beschleunigen und Zeit und Kosten zu sparen, da sich Fehler früher in der Validierungs- und Verifizierungsphase identifizieren lassen.
Formale Verifikation in der Praxis
Die Vorteile der formalen Verifizierung sind nicht nur theoretischer Natur – sie haben sich in zahlreichen praktischen Anwendungen bewährt. Unsere Kunden berichten, dass die häufigsten „potenziell schwerwiegenden Fehler“ Zugriffe auf nicht initialisierte Variablen sowie Off-by-One-Fehler sind. Da diese Fehler vor der Produktion entdeckt werden, ist der tatsächliche Schaden, den sie hätten verursachen können, schwer abzuschätzen. Er kann jedoch von einer einfachen Fehlfunktion bis hin zu einer verheerenden Sicherheitslücke reichen.
Anzeige
In der Reihe „Code Unboxed“ stellen Experten von TrustInSoft Open-Source-Software auf den Prüfstand. In Beispielen wie Tiny Crypt fand das Team sechs Fehler, darunter einen in den eigenen Tests. Sie betonen, wie wichtig formale Methoden für die gründliche Überprüfung von Speicher-Sicherheitslücken sind, die sehr subtil sein können und nur unter bestimmten Umständen auftreten, die mit herkömmlichen Tests nicht erfasst werden können.
Formale Verifikation kann dazu beitragen, die Sicherheit und Zuverlässigkeit von KI-Algorithmen in Embedded-Systemen zu gewährleisten. KI stellt in diesem speziellen Fall ein Risiko dar: Menschen, die KI für die Programmierung einsetzen, sind nicht mehr die Designer/Logiker/Künstler des Codes, sondern lediglich Prüfer. Folglich besteht ein höheres Risiko subtiler Sicherheitsauswirkungen bei der Verwendung von KI-generiertem Code. Daher ist es äußerst wichtig, entweder formale Verifizierungstools zur Überprüfung, gründlichere manuelle Überprüfungen oder beides einzusetzen.
Anzeige
Zusammenarbeit ist entscheidend
Die Entwicklung von Embedded-Software ist oft eine gemeinschaftliche Aufgabe, an der Teams von Entwicklern arbeiten, die sich mit verschiedenen Teilen des Systems beschäftigen. Formale Verifizierung kann diese Zusammenarbeit erleichtern, indem sie eine standardisierte Methode für die Diskussion und Verifikation von Code bereitstellt. Durch die Verwendung formaler Spezifikationen und Verifizierungstools können Entwickler ihre Absichten klar kommunizieren und sicherstellen, dass sich ihr Code nahtlos in den Rest des Systems einfügt.
Mit TrustInSoft Analyzer lassen sich Laufzeitfehler, Speicherlecks und Schwachstellen beseitigen und so Entwicklungskosten und Markteinführungszeiten reduzieren. Darüber hinaus wird die Einhaltung von Industriestandards gesichert und aufrechterhalten und durch überprüfbare Codeintegrität das Vertrauen in Ihre Embedded-Systeme aufgebaut.
Was bringt die Zukunft bei Embedded-Systemen?
Die Nachfrage nach robusten Embedded-Systemen wird weiter steigen. Da wir immer mehr Bereiche unseres Lebens der Software anvertrauen, ist formale Verifikation kein Luxus mehr, sondern eine grundlegende Anforderung. TrustInSoft steht Ihnen als Partner zur Seite und bietet die Tools und das Fachwissen, um sich in dieser komplexen Landschaft zurechtzufinden und eine Zukunft zu gestalten, in der Embedded-Systeme wirklich sicher und zuverlässig sind. (na)
