1. Home
  2. Electronics (German)
  3. Tod durch Softwarefehler
  4. Page 3

Tod durch Softwarefehler

Interessanter Talk, aber 100% Korrektheit ist nicht möglich. Die Korrektheit eines Programms kann nur beweisen, daß es einer (formalen) Spezifikation entspricht. Aber Spezifikationen halten nicht immer den Kontakt mit der realen Welt stand.

Sprachen wie Haskell oder Erlang und die Konzept wie Lambda Calculus mit besser entwickelten Typ-Theorien, helfen allerdings bei vielen Problemen, wie Speicherproblemen, Buffer-Overflows usw., was Programme schon sicherer machen kann. Aber gibt es Haskell für Embedded Systeme und kann man harte Realtime damit programmieren?

CompCert, oder das SAFE-Projekt, angelehnt an Lisp-Maschinen, klingen allerdings nach guten Entwicklungen, sollte man im Auge behalten. Wird aber wohl noch ein paar Jahrzehnte dauern, bevor solche besseren Konzepte in der Industrie ankommen, wenn überhaupt. Lisp-Maschinen (und alle Konzepte davon) sind ja sogar wieder in der Versenkung verschwunden.

All das hilft aber nicht bei fehlerhaften Spezifikationen. Ein Beispiel wären Cross-Site-Scripting Attacken. Es werden perfekt alle HTML-Standards usw. eingehalten, es gibt keine klassische Angriffe durch Fehler in C-Programmen, aber durch eine Lücke in der Spezifikation einer Webanwendung (bestimmten HTML-Code nicht zu filtern) sind solche Angriffe möglich. Natürlich würde heutzutage solche Fehler keiner mehr machen, aber je komplexer ein System ist, umso komplexer sind auch die Fehler- und Angriffsmöglichkeiten und es werden garantiert immer neue entdeckt.

--
Frank Buss, http://www.frank-buss.de 
electronics and more: http://www.youtube.com/user/frankbuss
Reply to
Frank Buss
Loading thread data ...

Vor allem ist auch die Frage ob die Spezifikation korrekt ist. Irgendwer hat sie geschrieben, normalerweise ein Mensch, Menschen machen Fehler.

Dann darf man auch nicht vergessen, daß, selbst wenn der Source komplett korrekt ist, man schliesslich nicht den Source ausführt sondern das Compilat und das kann nur dann als korrekt angesehen werden wenn der Compiler selbst zu 100% verifiziert wurde. Welcher Compiler ist das? Ich leser immer wieder von Compilerfehlern wo eigentlich harmlos aussehender Code nicht zu dem compiliert was man erwarten würde.

Gerrit

Reply to
Gerrit Heitsch

Da soll CompCert helfen:

formatting link

Laut dem Vortrag wurde GCC, LLVM (MacOSX Compiler) und CompCert mit Compiler Fuzzing getestet (nach bestimmten Regeln zufällig generierter Code, der dann auf korrekte Compilierung getestet wurde). GCC und LLVM sollen hunderte von Fehlern gehabt haben. CompCert dageben nur 11, bedingt durch ein Parser-Modul, was nicht nach den strengen Regeln des restlichen Compilers programmiert worden war, was kurzfristig behoben wurde und er soll dann keine Fehler mehr gehabt haben.

Aber müsste man im Hinblick auf Embedded-System wohl nochmal gut testen, denn der Code ist ja meist immer noch korrekt compiliert, wenn Befehle umsortiert werden, was bei Microcontroller-Registerzugriffen nicht immer gut ist.

--
Frank Buss, http://www.frank-buss.de 
electronics and more: http://www.youtube.com/user/frankbuss
Reply to
Frank Buss

Aha... nur wenn das erzeugter Code ist, wie ist dann bekannt welches das korrekte Ergebnis der Compilation ist? Irgendein Compiler muss die Referenz geliefert haben (von Hand wirds keiner gemacht haben) und die Frage ist, liefert der wirklich korrekten Code?

Ich sehe da ein gewisses Henne/Ei-Problem auch wenn man mit diesem Ansatz sicher viele Bugs finden kann.

Ja, die CPU selbst spielt da auch noch rein. Wer erinnert sich noch an den POPAD-Bug im 386? Korrektes Programm (laut Spec), trotzdem Datenmüll.

Gerrit

Reply to
Gerrit Heitsch

Interessante Ideen, aber bis ich ein danach gebautes System im realen Betrieb gesehen habe, bleiben einige Zweifel. Bisher war es immer so, daß die reine Lehre den Kontakt mit der Realität nicht überlebt hat.

Und die Aussage am Ende, daß wenn man alte Programme aus der Zeit vor dem sicheren System benutzen will/muss, man einen zweiten Rechner braucht stellt schon fast sicher, daß es aktuelle Systeme nicht ersetzen wird.

Gerrit

Reply to
Gerrit Heitsch

Dann haben die Engländer, die sich am ECU-Code vom TDCi ausgetobt haben, aber seeeeehr klein gehalten. Ein Bekannter, der mit dem gleichen Basismotor, aber unterdruckbetätigter Abgasrückführung in seinem Mondeo rumgurkt, hat das defekte AGR-Ventil am Verbrauch gemerkt. Ich daran, dass ich mit blinkender Glühwendel äusserst langsam und äusserst geräuschintensiv mit dem Katzenauto über die Reeperbahn gehopst bin. Not_lauf_programm würde ich das jetzt nicht nennen. Defekt war auch nur das - hier aber elektronisch betätigte - AGRV.

Ja und die andere Hälfte liegt dem Fahrer betriebswarm auf dem Schoß. Das käme dann in etwa hin.

Reply to
Stefan Huebner

Dazu kommen dann aber ein paar zehn Euro extra für ein Board mit Chipsatz, der ECC unterstützt. Ich habe es mehr zufällig in meiner Workstation - ein Quadcore Xeon musste untergebracht werden :) Aber absichtlich gekauft habe ich sowas bisher noch nie...

Reply to
Stefan Huebner

Am 28.10.2013 17:13, schrieb Gerrit Heitsch:

Och, der Sechszylinder wird meine Karre dann schon noch bewegen :-)

Butzo

Reply to
Klaus Butzmann

Am 28.10.2013 22:30, schrieb Frank Buss:

Zugegeben.

Das ist ein Henne-Ei-Problem: Solange du keinen Bedarf an sowas hast, wird es auch nicht entwickelt werden. Bisher war C gut genug.

Die Komplexität ist heute schon um ein Irrsinniges zu hoch. Wer auf sowas Beklopptes kommt, wie JavaScript in PDF einzubauen, oder überhaupt JavaScript - Daten mit Code vermischen, der dann lokal ohne Rückfrage bei dir ausgeführt wird - der muß sich nicht wundern. Daß JS ein Rezept für Desaster ist war mir klar, als ich das erste Mal davon gehört habe.

Dennoch: Wenn ich eine VM auf meinem Rechner habe, die verifizierterweise niemals nie nicht außerhalb ihres Scope auch nur ein Bit an meinem Rechner verändert, wäre mir wohler. Denn bösartiger Code kann auch aus heutigen Virtualisierungen ausbrechen.

Außerdem müßte man an einem System mit einem Grundstock verifizierten Codes nicht alle naselang rumpatchen - was ja auch ein potentielles Einfallstor von Schadsoft ist.

Hanno

Reply to
Hanno Foest
äAm 28.10.2013 23:17, schrieb Gerrit Heitsch:

Soweit ich das verstenden habe - ist etwas her, daß ich den Vortrag gehört habe - hat man in der Tat den Kram mit händisch verifiziertem Code gebootstrappt.

Du brauchst auch entsprechende spezielle (verifizierte) Hardware...

Hanno

Reply to
Hanno Foest

Gerrit Heitsch schrieb:

Beim GCC hatte ich Fall, dass die Optimierung das Programm zermurkst hat. Von den drei Optimierungsstufen "more, most, size" nehme ich seit dem immer nur die "schwächste" (was übrigens auch empfohlen wird).

Reply to
Edzard Egberts

Seitdem der Speichercontroller in der CPU ist, ist das nicht mehr Sache des Chipsets sondern der CPU. Leider hat sich INTeL dieses Feature bei den Desktop-CPUs gespart, man braucht einen XEON. AMD hingegen hat es in allen normalen CPUs drin (bei den APUs anscheinend nicht), da braucht es nur ein Mainboard mit den passenden Leiterbahnen und BIOS. ASUS z.B.

Ich schon. Genau weil ich schon schwer zu findende Fehler mit RAM hatte und darauf keine Lust mehr habe. Auch ist das RAM von besserer Qualität wenn es ECC kann. Schliesslich wird jeder erkannte Fehler gnadenlos dem OS gemeldet, macht es schwer RAMsch zu verkaufen.

Gerrit

Reply to
Gerrit Heitsch

Ja, aber nicht mehr sehr gut... Mehr als 120 auf ebener Strecke (und 80 leicht bergauf) waren einfach nicht mehr drin als mir das passierte. Wer das noch nicht erlebt hat glaubt es nicht.

Gerrit

Reply to
Gerrit Heitsch

Das ist leider nicht zu 100% machbar. Wie POPAD zeigt müsstest du jede mögliche Befehlskombination testen. Andere CPU-Bugs die rauskamen nahmen auch noch Bezug auf Registerinhalte. Das bist du ganz schnell bei einer Menge von Kombinationen die auch die schnellste CPU nicht in brauchbarer Zeit durchprobiert.

Nachdem eine CPU Hardware ist, müsstest du diese Verifikation bei jeder produzierten CPU machen. Könnte schliesslich ein kleiner Fehler in der Maske sein der einen Bug einbaut der nicht immer auftritt sondern nur wenn bestimmte Dinge bei der Produktion (Dotierung, Position auf dem Wafer) und später im Betrieb zusammenkommen.

Gerrit

Reply to
Gerrit Heitsch

Am Tue, 29 Oct 2013 08:09:26 +0100 schrieb Edzard Egberts:

Was ist da konkret passiert? Bei mir stellten sich in Betracht gezogene 'Compilerfehler' nach genauerer Untersuchung eigentlich immer wieder als eigene Denkfehler heraus.

Lutz

--
Mit unseren Sensoren ist der Administrator informiert, bevor es Probleme im  
Serverraum gibt: preiswerte Monitoring Hard- und Software-kostenloses Plugin  
auch für Nagios - Nachricht per e-mail,SMS und SNMP: http://www.messpc.de 
Messwerte nachträgliche Wärmedämmung http://www.messpc.de/waermedaemmung.php
Reply to
Lutz Schulze

Frank Buss schrieb:

Für in ADA geschriebene Programme gibt es das SPARK-System. Da wird ähnlich wie bei "Design by Contract" jede Funktion mit Prüfregeln angereichert. IIRC werden erlaubter PArameterbereich und erlaubte bzw. mögliche Ausgabewerte angegeben.

Was da über statische Prüfung wie bei MISRA-C hinaus möglich ist, m üßte man sich aus der einschlägigen Doku raussuchen. An Stackprüfung bzw.

-überwachung erinnere ich mich nicht, aber mein Kontakt damit ist auch sehr lange her, Weiterentwicklung nicht ausgeschlossen ...

Marc

Reply to
Marc Santhoff

Ja, wie damals als MS ActiveX brachte... Was kann schon schiefgehen wenn eine Website bei dir x86 Code ausführen darf?

Daten und Code sollte man getrennt halten. Aber auch das ist nicht mehr machbar, weil sich sonst die ganzen Anwender von Office lautstark beschweren, daß ihre ganzen Macros nicht mehr funktionieren.

Problem ist dann ein anderes. Wenn es jemand doch schafft ein neues Einfallstor zu finden weil nie jemand diesen neuen Weg auch nur angedacht hat, dann wirst du in dasselbe Problem reinlaufen wie damals bei den PINs der EC-Karten.

"Laut unseren Unterlagen benutzen sie 'Total-sicher-OS'(TM), also muss der Fehler bei ihnen liegen, wir lehnen jegliche Haftung ab"

Gerrit

Reply to
Gerrit Heitsch

Lutz Schulze schrieb:

Mit PC ein Programm für ein Linux-Board compiliert - lief auf dem PC, aber nicht auf dem Board. Weniger optimiert lief es dann auch auf dem Board. Woran genau das lag, habe ich dann nicht untersucht - Betriebssystem und Software auf PC und Board gleich, könnte eine Prozessor-Optimierung gewesen sein.

Da habe ich eine übersehen, es sind "none, optimize, more, most, size" (00, 01, 02, etc.) und empfohlen ist "more" (02).

Reply to
Edzard Egberts

Am 29.10.2013 08:30 schrieb Gerrit Heitsch:

Wenn du die Hardare auf Verifizierbakeit hin designst hast du bessere Karten.

Der ist dann aber nicht gezielt exploitbar, weil man sich nicht drauf verlassen kann.

Hanno

Reply to
Hanno Foest

Am 29.10.2013 08:45 schrieb Gerrit Heitsch:

Das ist ein soziales Problem, das man nicht mit technischen Mitteln angehen kann. Wie dein Beispiel zeigt, gibt es das Problem bereits bei "normal unsicheren" Systemen. Ich seh jetzt aber gar nicht ein, mit weniger Sicherheit als möglich zu arbeiten, nur weil mir irgendein Spinner einen Strick draus drehen könnte.

Hanno

Reply to
Hanno Foest

ElectronDepot website is not affiliated with any of the manufacturers or service providers discussed here. All logos and trade names are the property of their respective owners.