Antonov 225 - größtes Flugzeug der Welt, mit 640 t Startgewicht - Zerstört!...

[Thomas Prufer]

On Wed, 30 Mar 2022 20:57:10 +0200, Helmut Schellong <rip@schellong.biz> wrote:

Trotzdem reicht ein Test x=0 y=15 aus, um die Korrektheit
der Implementation zu beweisen.
Jeder beliebige einzelne Test reicht dazu aus!

Da feits vom Boa weg.

Appendix A: Test Vectors

This is a set of test vectors for conformance testing, given in octet
form.

.... and I don\'t really think your English is up to the fine distinction between
conformance testing and mathematical proof...

Thomas Prufer

 

[Marc Haber]

Josef Moellers <josef.moellers@invalid.invalid> wrote:

Nein. Es gibt keinen Test, der die Korrektheit eines Codes (d.h.
Algorithmus UND Implementation) *beweisen* kann!
Das ist allgemein bekannt und ich möchte mal behaupten, dessen sind sich
die Entwickler des Codes auch bewußt.

Die theoretische Informatik wird Dir da seit 40 Jahren vehement
widersprechen.

Die Problematik ist halt, dass die formale Verifikation eines
Programms auf Spezifikationsgerechtheit und korrekter Implementation
schreiend aufwendig ist und nur dann Sinn ergibt, wenn man das
Programm dann mit einem verifizierten Compiler übersetzt, mit
verifizierten Libraries linkt und auf einer mit verifizierter Firmware
versorgten verifizierten CPU ausführt.

Und _DAS_ ist ein Beschaffungsproblem.

Grüße
Marc
--
-------------------------------------- !! No courtesy copies, please !! -----
Marc Haber | \" Questions are the | Mailadresse im Header
Mannheim, Germany | Beginning of Wisdom \" |
Nordisch by Nature | Lt. Worf, TNG \"Rightful Heir\" | Fon: *49 621 72739834

 

[Gerrit Heitsch]

On 3/31/22 12:59, Marc Haber wrote:

Josef Moellers <josef.moellers@invalid.invalid> wrote:
Nein. Es gibt keinen Test, der die Korrektheit eines Codes (d.h.
Algorithmus UND Implementation) *beweisen* kann!
Das ist allgemein bekannt und ich möchte mal behaupten, dessen sind sich
die Entwickler des Codes auch bewußt.

Die theoretische Informatik wird Dir da seit 40 Jahren vehement
widersprechen.

Die Problematik ist halt, dass die formale Verifikation eines
Programms auf Spezifikationsgerechtheit und korrekter Implementation
schreiend aufwendig ist und nur dann Sinn ergibt, wenn man das
Programm dann mit einem verifizierten Compiler übersetzt, mit
verifizierten Libraries linkt und auf einer mit verifizierter Firmware
versorgten verifizierten CPU ausführt.

Und _DAS_ ist ein Beschaffungsproblem.

Mag sein... Ich denke aber, Bodenproben von Pluto wären einfacher zu
beschaffen.

Gerrit

 

[Bernd Laengerich]

Am 30.03.2022 um 18:21 schrieb Gerrit Heitsch:

Bisher hat sich leider oft gezeigt, daß obige Behauptungen nur bedeuten, daß
man noch nicht genau genug gemessen hat. Mit Glitching hat man auch schon
einigen als sicher verkauften Chips Daten entlocken können.

Sicher gibt es auch hier Angriffsvektoren, sie sind aber meist schonmal
deutlich aufwendiger als einfach nur von außen beobachten. Und die Schutzstufe
wird von normalen Prozessoren einfach nicht erreicht.
Ja, ich kenne den DigiCipher-2-Hack Das war aber auch ein Consumergerät für
$3,50 aus den 90ern auf Basis eines 6502, die Zeit ist da auch nicht
stehengeblieben (Wer mal forschen möchte: Ich habe noch etliche obsolete
PIN-Pads aus den 90ern). Und das die Schlüssel 25a lang nicht ausgelesen
wurden zeigt daß die Qualität offenbar gar nicht so schlecht war.

Wenn Du an den Prozessor herankommst ist es normalerweise schon zu spät. Die
Prozessoren sitzen wiederum in einer Schutzumhausung, die bei Öffnen sämtliche
gespeicherten Schlüssel löscht. Klassisch ist das z.B. eine vollständige ,
ggf. mehrschichtige, Umhüllung aus Kapton mit mäanderförmigen Leiterbahnen,
dazu in der weiteren Umhüllung verborgene Kontakte, Lichtsensoren.

Ins Rechenzentrum kommen ohne Einbruch nur auditierte Personen, das Gerät ist
im Rack mit 2 Schlössern angeschlossen, diese sind mit Alarmsensoren überwacht.
Und es wird der Betrieb überwacht, auch die Nichterreichbarkeit eines Gerätes
ist ein Alarmsignal.

Bernd

 

[Bernd Laengerich]

Am 31.03.2022 um 12:59 schrieb Marc Haber:

Die Problematik ist halt, dass die formale Verifikation eines
Programms auf Spezifikationsgerechtheit und korrekter Implementation
schreiend aufwendig ist und nur dann Sinn ergibt, wenn man das
Programm dann mit einem verifizierten Compiler übersetzt, mit
verifizierten Libraries linkt und auf einer mit verifizierter Firmware
versorgten verifizierten CPU ausführt.

Ada hat sich wohl nie so richtig durchgesetzt, ist nicht Hip genug. Da gibt es
schliesslich zertifizierte Umgebungen. In sicherheitsrelevanten Bereichen wird
Ada allerdings verwendet. Bezeichnend dazu: \"Bis auf einzelne Ausnahmen
verweigert sich die Automobilindustrie ihrer Verwendung\"
Man kann schliesslich auch in Whitespace oder Brainfuck coden, wenn es zwar
keine Sicherheit aber \"Fahrerlebnis\" verspricht...

Bernd

 

[Eric Bruecklmeier]

Am 31.03.2022 um 13:16 schrieb Bernd Laengerich:

Wenn Du an den Prozessor herankommst ist es normalerweise schon zu spät.
Die Prozessoren sitzen wiederum in einer Schutzumhausung, die bei Öffnen
sämtliche gespeicherten Schlüssel löscht. Klassisch ist das z.B. eine
vollständige , ggf. mehrschichtige, Umhüllung aus Kapton mit
mäanderförmigen Leiterbahnen, dazu in der weiteren Umhüllung verborgene
Kontakte, Lichtsensoren.

https://patentimages.storage.googleapis.com/74/9b/2b/c8da3187a5e361/US6452283.pdf

 

[Helmut Schellong]

On 03/31/2022 07:52, Thomas Prufer wrote:

On Wed, 30 Mar 2022 20:57:10 +0200, Helmut Schellong <rip@schellong.biz> wrote:

Trotzdem reicht ein Test x=0 y=15 aus, um die Korrektheit
der Implementation zu beweisen.
Jeder beliebige einzelne Test reicht dazu aus!

Da feits vom Boa weg.


Appendix A: Test Vectors

This is a set of test vectors for conformance testing, given in octet
form.

... and I don\'t really think your English is up to the fine distinction between
conformance testing and mathematical proof...

http://www.schellong.de/htm/kern.c.html
https://datatracker.ietf.org/doc/html/rfc4503
https://cr.yp.to/streamciphers/rabbit/desc.pdf

Wer die drei Inhalte gründlich zur Kenntnis nimmt, wird erkennen, daß durch
Durchführung aller Tests mit jeweils festgestellter Übereinstimmung, (eigentlich)
zwingend ein Beweis für eine korrekte Implementation vorliegt.

|The IV addition modifies the counter values in such a way that it can
|be guaranteed that under an identical key, all 2^64 possible different IVs
|will lead to unique keystreams.



--
Mit freundlichen Grüßen
Helmut Schellong var@schellong.biz
http://www.schellong.de/c.htm http://www.schellong.de/c2x.htm http://www.schellong.de/c_padding_bits.htm
http://www.schellong.de/htm/bishmnk.htm http://www.schellong.de/htm/rpar.bish.html http://www.schellong.de/htm/sieger.bish.html
http://www.schellong.de/htm/audio_proj.htm http://www.schellong.de/htm/audio_unsinn.htm http://www.schellong.de/htm/tuner.htm
http://www.schellong.de/htm/string.htm http://www.schellong.de/htm/string.c.html http://www.schellong.de/htm/deutsche_bahn.htm
http://www.schellong.de/htm/schaltungen.htm http://www.schellong.de/htm/rand.htm http://www.schellong.de/htm/bsd.htm

 

[Reinhardt Behm]

On Thu, 31 Mar 2022 12:59:04 +0200, Marc Haber wrote:

Josef Moellers <josef.moellers@invalid.invalid> wrote:
Nein. Es gibt keinen Test, der die Korrektheit eines Codes (d.h.
Algorithmus UND Implementation) *beweisen* kann!
Das ist allgemein bekannt und ich möchte mal behaupten, dessen sind sich
die Entwickler des Codes auch bewußt.

Die theoretische Informatik wird Dir da seit 40 Jahren vehement
widersprechen.

Die Problematik ist halt, dass die formale Verifikation eines Programms
auf Spezifikationsgerechtheit und korrekter Implementation schreiend
aufwendig ist und nur dann Sinn ergibt, wenn man das Programm dann mit
einem verifizierten Compiler übersetzt, mit verifizierten Libraries
linkt und auf einer mit verifizierter Firmware versorgten verifizierten
CPU ausführt.

Und _DAS_ ist ein Beschaffungsproblem.

Grüße Marc

Typisch macht man die Verification mit dem compilierten Code möglichst
auf der Zielhardware. Damit werden auch Compiler-Bugs erwischt und auch
eventuelle CPU-Bugs.

Man muss natürlich sicherstellen, dass spätere Hardware äquivalent zur
der ist, die für die Verifikation benutzt wurde.

--
Reinhardt

 

[Hanno Foest]

Am 31.03.22 um 12:59 schrieb Marc Haber:

Die Problematik ist halt, dass die formale Verifikation eines
Programms auf Spezifikationsgerechtheit und korrekter Implementation
schreiend aufwendig ist und nur dann Sinn ergibt, wenn man das
Programm dann mit einem verifizierten Compiler übersetzt, mit
verifizierten Libraries linkt und auf einer mit verifizierter Firmware
versorgten verifizierten CPU ausführt.

https://github.com/SymbioticEDA/riscv-formal
https://trustworthy.systems/projects/seL4-verification/

> Und _DAS_ ist ein Beschaffungsproblem.

Geht so - inzwischen gibt es da schon ein paar Dinge.

Und es ist zwar richtig, daß man sowas für die Verifikation des
Gesamtsystems braucht, aber wenn der Scope nur die Verifikation des
Codes ist, kann man die Korrektheit des Rests einfach voraussetzen. An
irgendeiner Stelle muß man eh eh einen Schnitt machen - ob die Physik
des benutzten Prozessorexemplars nun wirklich der Theorie folgt, oder ob
da ein winziger Produktionsfehler ein schwer zu entdeckendes und selten
auftretendes Problem in Form einer Abweichung zur Theorie erzeugt, kann
man eh nicht mit mathematischen Methoden herausfinden.

Hanno

--
The modern conservative is engaged in one of man\'s oldest exercises in
moral philosophy; that is, the search for a superior moral justification
for selfishness.
- John Kenneth Galbraith

 

[Marc Haber]

Reinhardt Behm <rbehm@hushmail.com> wrote:

On Thu, 31 Mar 2022 12:59:04 +0200, Marc Haber wrote:

Josef Moellers <josef.moellers@invalid.invalid> wrote:
Nein. Es gibt keinen Test, der die Korrektheit eines Codes (d.h.
Algorithmus UND Implementation) *beweisen* kann!
Das ist allgemein bekannt und ich möchte mal behaupten, dessen sind sich
die Entwickler des Codes auch bewußt.

Die theoretische Informatik wird Dir da seit 40 Jahren vehement
widersprechen.

Die Problematik ist halt, dass die formale Verifikation eines Programms
auf Spezifikationsgerechtheit und korrekter Implementation schreiend
aufwendig ist und nur dann Sinn ergibt, wenn man das Programm dann mit
einem verifizierten Compiler übersetzt, mit verifizierten Libraries
linkt und auf einer mit verifizierter Firmware versorgten verifizierten
CPU ausführt.

Und _DAS_ ist ein Beschaffungsproblem.

Grüße Marc

Typisch macht man die Verification mit dem compilierten Code möglichst
auf der Zielhardware. Damit werden auch Compiler-Bugs erwischt und auch
eventuelle CPU-Bugs.

Man muss natürlich sicherstellen, dass spätere Hardware äquivalent zur
der ist, die für die Verifikation benutzt wurde.

Formale Verifikation macht man am Schreibtisch.

--
-------------------------------------- !! No courtesy copies, please !! -----
Marc Haber | \" Questions are the | Mailadresse im Header
Mannheim, Germany | Beginning of Wisdom \" |
Nordisch by Nature | Lt. Worf, TNG \"Rightful Heir\" | Fon: *49 621 72739834

 

[Josef Moellers]

On 31.03.22 12:59, Marc Haber wrote:

Josef Moellers <josef.moellers@invalid.invalid> wrote:
Nein. Es gibt keinen Test, der die Korrektheit eines Codes (d.h.
Algorithmus UND Implementation) *beweisen* kann!
Das ist allgemein bekannt und ich möchte mal behaupten, dessen sind sich
die Entwickler des Codes auch bewußt.

Die theoretische Informatik wird Dir da seit 40 Jahren vehement
widersprechen.

Seltsam ... tut sie nicht.

Die Problematik ist halt, dass die formale Verifikation eines
Programms auf Spezifikationsgerechtheit und korrekter Implementation
schreiend aufwendig ist und nur dann Sinn ergibt, wenn man das
Programm dann mit einem verifizierten Compiler übersetzt, mit
verifizierten Libraries linkt und auf einer mit verifizierter Firmware
versorgten verifizierten CPU ausführt.

Es wird da eine zweistufige Vorgehensweise geben:
1) Die Korrektheit des Algorithmus\' wird formal mathematisch-logisch
bewiesen
2) Jede Implementation wird mittels aufwendiger Tests *verifiziert*.
D.h. es besteht immer noch die Möglichkeit, daß ein *Implementation*
nicht korrekt ist.
Für einen sicherheitskritischen Algorithmus, wie es ein
verschlüsselungsverfahren ist, erwarte ich Ersteres.

> Und _DAS_ ist ein Beschaffungsproblem.

Im Endeffekt ist alles eine Kostenfrage. Auch der formale Beweis der
Korrektheit eines Algorithmus und dann auch noch der Implementation
scheitert i.d.R. an den Kosten.

Josef

 

[Volker Bartheld]

On Thu, 31 Mar 2022 18:23:37 +0200, Hanno Foest wrote:

Und es ist zwar richtig, daß man sowas für die Verifikation des
Gesamtsystems braucht, aber wenn der Scope nur die Verifikation des
Codes ist, kann man die Korrektheit des Rests einfach voraussetzen. An
irgendeiner Stelle muß man eh eh einen Schnitt machen - ob die Physik
des benutzten Prozessorexemplars nun wirklich der Theorie folgt, oder ob
da ein winziger Produktionsfehler ein schwer zu entdeckendes und selten
auftretendes Problem in Form einer Abweichung zur Theorie erzeugt, kann
man eh nicht mit mathematischen Methoden herausfinden.

Oder ob in der Hardware eine Backdoor eingebaut wurde.

https://wccftech.com/intel-possibly-amd-chips-permanent-backdoors-planted-nsa-updated-1/
https://www.realworldtech.com/forum/?threadid=35566&curpostid=35566
https://es.slideshare.net/ortegaalfredo/deep-submicronbackdoorsortegasyscan2014slides
https://www.borncity.com/blog/2018/08/12/black-hat-alte-x86-via-cpu-frs-militr-mit-backdoor/
https://www.theregister.com/2018/08/10/via_c3_x86_processor_backdoor/
https://www.blackhat.com/us-18/briefings/schedule/index.html#god-mode-unlocked---hardware-backdoors-in-x-cpus-10194
https://hackaday.com/2020/06/16/disable-intels-backdoor-on-modern-hardware/
https://defcon.org/images/defcon-20/dc-20-presentations/Brossard/DEFCON-20-Brossard-Hardware-Backdooring-is-Practical.pdf
https://www.tweaktown.com/news/24383/us_military_chip_made_in_china_has_security_backdoor_massive_national_security_concerns/index.html
https://www.computerworld.com/article/3079417/researchers-built-devious-undetectable-hardware-level-backdoor-in-computer-chips.html
https://www.wired.com/2016/06/demonically-clever-backdoor-hides-inside-computer-chip/

Volker

 

[Hanno Foest]

On 01.04.22 11:03, Volker Bartheld wrote:

> Oder ob in der Hardware eine Backdoor eingebaut wurde.

[URLs]

Da fehlt noch der Klassiker:

https://sharps.org/wp-content/uploads/BECKER-CHES.pdf

Aber ja, klar. Absicht kommt noch zu den ungewollten Fehlermöglichkeiten
hinzu. Läßt sich aber darunter subsumieren, daß die Physik nicht der
Theorie (des originalen Designers) folgt.

Hanno

--
The modern conservative is engaged in one of man\'s oldest exercises in
moral philosophy; that is, the search for a superior moral justification
for selfishness.
- John Kenneth Galbraith

 

[Volker Bartheld]

On Fri, 1 Apr 2022 11:18:41 +0200, Hanno Foest wrote:

On 01.04.22 11:03, Volker Bartheld wrote:
Oder ob in der Hardware eine Backdoor eingebaut wurde.
[URLs]
Da fehlt noch der Klassiker:
https://sharps.org/wp-content/uploads/BECKER-CHES.pdf

Richtig. Danke! Den hatte ich vergessen. Eine echte Perle. Sind natürlich
in der Gesamtschau alles recht ausgefuchste Sachen, derer sich Experten
annehmen müssen und meilenweit von der Aussage entfernt, man könnte anhand
einer Stichprobe die \"korrekte\" Implementierung eines Algorithmus (was auch
immer unter korrekt zu verstehen ist, das Stichwort \"Seitenkanalattacke\"
wurde ja bereits gegeben und nicht verstanden) beweisen.

Aber ja, klar. Absicht kommt noch zu den ungewollten Fehlermöglichkeiten
hinzu. Läßt sich aber darunter subsumieren, daß die Physik nicht der
Theorie (des originalen Designers) folgt.

Ich finde ja eigentlich diejenigen Sabotagemöglichkeiten (die
sicherheitsrelevante Kompromittierung eines Systems ist ja auch eine
Variante von Sabotage) am spannendsten, wo der Saboteur (gerne auch
Insider) einfach nur eine Zeile anscheinend vollkommen harmlosen Code
einfügen muß (Sleep z. B.), ein bisserl was an der Ausführungsreihenfolge
oder den Startparametern drehen oder die Specs grenzwertig auslegen muß.

Also ohne nachweisbaren Vorsatz, jeder tat sein Möglichstes.

Vor dem Hintergrund war es auch schlauer, im Abgasskandal das
\"Thermofenster\" (für die spezifikationsgemäße Funktion des Katalysators)
auf [20.0°C;22.0°C] zu definieren, als irgendwelche skurrilen
Prüfstandserkennungs- und Abschalteinrichtung zu coden. Obwohl: In Zukunft
wird man einfach ein paar unscheinbare Parameter in irgendwelchen
Kennfeldern verbiegen und zum selben Ergebnis gelangen.

Hat mich ja sehr erstaunt, daß diese
Controlled-Misfire-Krachdeppen-Fehlzündungsfunktion
so vollkommen trivial zugänglich ist. Schubabschaltung oberhalb von x
U/min deaktivieren, Zündzeitpunkt für Drosselklappenwinkel <10% auf sehr
spät verschieben und fertig ist die Laube. Das legt man auf die
Klimaanlagenfunktion (separates Kennfeld, da meist mit
Leerlaufdrehzahlanhebung) und der Kerl mit Hoodiejopperl und Pudelmütze
kriegt einen Dauerständer.

Vollker

 

[Helmut Schellong]

On 04/01/2022 11:48, Volker Bartheld wrote:

On Fri, 1 Apr 2022 11:18:41 +0200, Hanno Foest wrote:
On 01.04.22 11:03, Volker Bartheld wrote:
Oder ob in der Hardware eine Backdoor eingebaut wurde.
[URLs]
Da fehlt noch der Klassiker:
https://sharps.org/wp-content/uploads/BECKER-CHES.pdf

Richtig. Danke! Den hatte ich vergessen. Eine echte Perle. Sind natürlich
in der Gesamtschau alles recht ausgefuchste Sachen, derer sich Experten
annehmen müssen und meilenweit von der Aussage entfernt, man könnte anhand
einer Stichprobe die \"korrekte\" Implementierung eines Algorithmus (was auch
immer unter korrekt zu verstehen ist, das Stichwort \"Seitenkanalattacke\"
wurde ja bereits gegeben und nicht verstanden) beweisen.

Ein Algorithmus ist korrekt implementiert, wenn für jede mögliche Eingabe
dessen Ausgabe übereinstimmend mit der Referenz-Implementation ist.
Vorstehend die allgemeine Antwort.

Bei ganz bestimmten Algorithmen können aufgrund von deren spezifischen Eigenschaften
Stichproben beweiskräftig die Korrektheit einer Implementation bestätigen.
Die jeweiligen Entwickler können eine geeignete Testprozedur festlegen.
Die allgemeinen Regeln sind dann im betreffenden Kontext nicht anwendbar.

Seiteneffekte diverser Art sind mir seit Jahrzehnten bekannt.
Insbesondere Programmiersprachen sind hierzu sehr affin.
Zu behaupten, ich würde solche nicht verstehen, ist albern.

Grotesk ist die Behauptung, daß kryptographische Algorithmen nicht selbst
implementiert werden sollen, weil dann Seitenkanäle negativ wirksam werden können.
Ein falsch implementierter Algorithmus bedarf keines Seitenkanalwirkens, um schädlich
zu wirken, sondern er generiert direkt defekte Ausgabedaten.
Einfach absurd!


--
Mit freundlichen Grüßen
Helmut Schellong var@schellong.biz
http://www.schellong.de/c.htm http://www.schellong.de/c2x.htm http://www.schellong.de/c_padding_bits.htm
http://www.schellong.de/htm/bishmnk.htm http://www.schellong.de/htm/rpar.bish.html http://www.schellong.de/htm/sieger.bish.html
http://www.schellong.de/htm/audio_proj.htm http://www.schellong.de/htm/audio_unsinn.htm http://www.schellong.de/htm/tuner.htm
http://www.schellong.de/htm/string.htm http://www.schellong.de/htm/string.c.html http://www.schellong.de/htm/deutsche_bahn.htm
http://www.schellong.de/htm/schaltungen.htm http://www.schellong.de/htm/rand.htm http://www.schellong.de/htm/bsd.htm

 

[Enrik Berkhan]

Helmut Schellong <rip@schellong.biz> wrote:

Grotesk ist die Behauptung, daß kryptographische Algorithmen nicht selbst
implementiert werden sollen, weil dann Seitenkanäle negativ wirksam werden können.
Ein falsch implementierter Algorithmus bedarf keines Seitenkanalwirkens, um schädlich
zu wirken, sondern er generiert direkt defekte Ausgabedaten.
Einfach absurd!

Grotesk und absurd ist vor allem dein fundiertes Missverständnis der
Begriffe.

 

[Hanno Foest]

On 01.04.22 11:48, Volker Bartheld wrote:

Ich finde ja eigentlich diejenigen Sabotagemöglichkeiten (die
sicherheitsrelevante Kompromittierung eines Systems ist ja auch eine
Variante von Sabotage) am spannendsten, wo der Saboteur (gerne auch
Insider) einfach nur eine Zeile anscheinend vollkommen harmlosen Code
einfügen muß (Sleep z. B.), ein bisserl was an der Ausführungsreihenfolge
oder den Startparametern drehen oder die Specs grenzwertig auslegen muß.

Also ohne nachweisbaren Vorsatz, jeder tat sein Möglichstes.

AKA \"Bugdoor\". Heartbleed ist da Referenzklasse.

Hanno

--
The modern conservative is engaged in one of man\'s oldest exercises in
moral philosophy; that is, the search for a superior moral justification
for selfishness.
- John Kenneth Galbraith

 

[Reinhardt Behm]

On Thu, 31 Mar 2022 20:42:12 +0200, Marc Haber wrote:

Reinhardt Behm <rbehm@hushmail.com> wrote:
On Thu, 31 Mar 2022 12:59:04 +0200, Marc Haber wrote:

Josef Moellers <josef.moellers@invalid.invalid> wrote:
Nein. Es gibt keinen Test, der die Korrektheit eines Codes (d.h.
Algorithmus UND Implementation) *beweisen* kann!
Das ist allgemein bekannt und ich möchte mal behaupten, dessen sind
sich die Entwickler des Codes auch bewußt.

Die theoretische Informatik wird Dir da seit 40 Jahren vehement
widersprechen.

Die Problematik ist halt, dass die formale Verifikation eines
Programms auf Spezifikationsgerechtheit und korrekter Implementation
schreiend aufwendig ist und nur dann Sinn ergibt, wenn man das
Programm dann mit einem verifizierten Compiler übersetzt, mit
verifizierten Libraries linkt und auf einer mit verifizierter Firmware
versorgten verifizierten CPU ausführt.

Und _DAS_ ist ein Beschaffungsproblem.

Grüße Marc

Typisch macht man die Verification mit dem compilierten Code möglichst
auf der Zielhardware. Damit werden auch Compiler-Bugs erwischt und auch
eventuelle CPU-Bugs.

Man muss natürlich sicherstellen, dass spätere Hardware äquivalent zur
der ist, die für die Verifikation benutzt wurde.

Formale Verifikation macht man am Schreibtisch.

Stimmt natürlich. Ich bin mehr mit DO178 (Avionics) beschäftigt. Da ist
formale Verifikation eher nicht die Regel.


--
Reinhardt

 

[Volker Bartheld]

On Fri, 1 Apr 2022 11:36:48 -0000 (UTC), Enrik Berkhan wrote:

Helmut Schellong <rip@schellong.biz> wrote:
Grotesk ist die Behauptung, daß kryptographische Algorithmen nicht
selbst implementiert werden sollen, weil dann Seitenkanäle negativ
wirksam werden können. Ein falsch implementierter Algorithmus bedarf
keines Seitenkanalwirkens, um schädlich zu wirken, sondern er generiert
direkt defekte Ausgabedaten. Einfach absurd!
Grotesk und absurd ist vor allem dein fundiertes Missverständnis der
Begriffe.

Grotesk ist auch, daß trotz mehrfacher Darlegung die mit NIHS
einhergehenden Schwierigkeiten nicht eingesehen wurden, von denen eine bei
der DIY-Implementierung von kryptografischen Algorithmen typischerweise die
Empfindlichkeit für Seitenkanalattacken ist. Das mit dem \"selbst
implementieren\" ist so ähnlich wie \"Bremsbeläge oder Räder am Kraftfahrzeug
selbst wechseln\": Hat man nicht das richtige Werkzeug, dauert es länger als
notwendig. Ist man nicht fachkundig, ist das Ergebnis möglicherweise
gefährliche Scheiße.

Und \"falsch implementiert\" darf gerne dehnbarer interpretiert werden.
Schellong erlaubt ja keinen Code-Review, daher kann von \"nach allen Regeln
der Kunst\" (meine Vermutung bei Universalgenies) über \"leicht ineffizient
und in die Jahre gekommen\" bis hin zu \"unwartbar schlampig hingerotzt\" und
schließlich \"haarsträubend fehlerhaft\" alles dabei sein.

Volker

 

[Bernd Laengerich]

Am 31.03.2022 um 13:29 schrieb Eric Bruecklmeier:

https://patentimages.storage.googleapis.com/74/9b/2b/c8da3187a5e361/US6452283.pdf

Lustig. Das zielt aber direkt auf Chips ab? Hat Sinn damit man auch die Chips
unter Spannung nicht abschleifen kann. Ich kenne ganze Sicherheitsmodule im
Wollknäuel, schon aus den 90ern.

Bernd