en
die Entwickler der Kontext-Algorithmen all ihre jeweiligen Angaben NUR zu den von ihnen entwickelten Algorithmen machen.
ntieren),
Diese Tatsache will man einfach nicht sehen und wahrhaben.
Frage gestellt werden kann, um argumentativ weiterzukommen.
sind.)
ragen.
nnen.
Einen nennenswerten Schaden habe ich noch nie angerichtet. Meine Entwicklungen hatten stets den Sollnutzen erbracht.
Das ist falsch, denn der Algorithmus
if Testverktor1 then return (Ergebnis-Testvektor1) else if Testverktor2 then return (Ergebnis-Testvektor2) else ... usw usf. else return(42)
nicht-Testvektoren.
Obiges ist ein *Beweis*, merke ich hier an...
Thomas Prufer
... so wie ich (und viele andere) nicht das beweisen anfangen, wenn wer ein funktionierendes perpetuum mobile behauptet.
Thomas Prufer
rgeben, auch alle weiteren
rden.
Ich sehe einen Syntax-Fehler...
--
Helmut Schellong snipped-for-privacy@schellong.biz
Am 30.03.22 um 15:01 schrieb Thomas Prufer:
Das ist elementare Erkenntnistheorie. Du kannst ja auch die These "alle
schwarze Schwan um die Ecke kommt.
Das obendrein...
Hanno
Das ist, sagen wir mal, "interessant".
rgeben, auch alle weiteren
rden.
Algorithmus:
y= 10*(x+1)+5; x=0..9999; (Referenz-Implementation)
Implementationsfehler:
10*(x+1)-5 10*(x+1)+4 11*(x+1)+5 10+(x+1)+5 10-(x+1)+5 9*(x+1)+5 10-(x+1)-5 10*(x+1)*5Trotzdem reicht ein Test x=0 y=15 aus, um die Korrektheit der Implementation zu beweisen. Jeder beliebige einzelne Test reicht dazu aus! Beispielsweise x=9975 y=99765 wird nur von einer korrekten Implemen tation generiert.
Die Entwickler eines Algorithmus werden fast immer in der Lage sein, ein einfaches Testverfahren zum Beweis einer korrekten Implementation auszuarbeiten. Sie kennen ihren Algorithmus! In diesem Fall sind alle existierenden allgemeinen Regeln in der Informat ik, die
etreffenden Algorithmus.
Auch zum Algorithmus Rabbit wurden Testdaten bereitgestellt, die aufgrund der
lich einen Beweis
========================= ========================= ========================= == Appendix A: Test Vectors
This is a set of test vectors for conformance testing, given in octet
form. For use with Rabbit, they have to be transformed into integers
by the conversion primitives OS2IP and I2OSP, as described in [5].
A.1. Testing without IV Setup
key = [00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00] S[0] = [B1 57 54 F0 36 A5 D6 EC F5 6B 45 26 1C 4A F7 02] S[1] = [88 E8 D8 15 C5 9C 0C 39 7B 69 6C 47 89 C6 8A A7] S[2] = [F4 16 A1 C3 70 0C D4 51 DA 68 D1 88 16 73 D6 96]
key = [91 28 13 29 2E 3D 36 FE 3B FC 62 F1 DC 51 C3 AC] S[0] = [3D 2D F3 C8 3E F6 27 A1 E9 7F C3 84 87 E2 51 9C] S[1] = [F5 76 CD 61 F4 40 5B 88 96 BF 53 AA 85 54 FC 19] S[2] = [E5 54 74 73 FB DB 43 50 8A E5 3B 20 20 4D 4C 5E]
key = [83 95 74 15 87 E0 C7 33 E9 E9 AB 01 C0 9B 00 43] S[0] = [0C B1 0D CD A0 41 CD AC 32 EB 5C FD 02 D0 60 9B] S[1] = [95 FC 9F CA 0F 17 01 5A 7B 70 92 11 4C FF 3E AD] S[2] = [96 49 E5 DE 8B FC 7F 3F 92 41 47 AD 3A 94 74 28]
A.2. Testing with IV Setup
mkey = [00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00] iv = [00 00 00 00 00 00 00 00] S[0] = [C6 A7 27 5E F8 54 95 D8 7C CD 5D 37 67 05 B7 ED] S[1] = [5F 29 A6 AC 04 F5 EF D4 7B 8F 29 32 70 DC 4A 8D] S[2] = [2A DE 82 2B 29 DE 6C 1E E5 2B DB 8A 47 BF 8F 66]
iv = [C3 73 F5 75 C1 26 7E 59] S[0] = [1F CD 4E B9 58 00 12 E2 E0 DC CC 92 22 01 7D 6D] S[1] = [A7 5F 4E 10 D1 21 25 01 7B 24 99 FF ED 93 6F 2E] S[2] = [EB C1 12 C3 93 E7 38 39 23 56 BD D0 12 02 9B A7]
iv = [A6 EB 56 1A D2 F4 17 27] S[0] = [44 5A D8 C8 05 85 8D BF 70 B6 AF 23 A1 51 10 4D] S[1] = [96 C8 F2 79 47 F4 2C 5B AE AE 67 C6 AC C3 5B 03] S[2] = [9F CB FC 89 5F A7 1C 17 31 3D F0 34 F0 15 51 CB]
Appendix B: Debugging Vectors
The following set of vectors describes the inner state of Rabbit during key and iv setup. It is meant mainly for debugging purposes. Octet strings are written according to I2OSP conventions.
B.1. Testing Round Function and Key Setup
key = [91 28 13 29 2E ED 36 FE 3B FC 62 F1 DC 51 C3 AC]
Inner state after key expansion: b = 0 X0 = 0xDC51C3AC, X1 = 0x13292E3D, X2 = 0x3BFC62F1, X3 = 0xC
3AC9128, X4 = 0x2E3D36FE, X5 = 0x62F1DC51, X6 = 0x91281329, X7 = 0x3 6FE3BFC, C0 = 0x36FE2E3D, C1 = 0xDC5162F1, C2 = 0x13299128, C3 = 0x3 BFC36FE, C4 = 0xC3ACDC51, C5 = 0x2E3D1329, C6 = 0x62F13BFC, C7 = 0x9 128C3ACInner state after first key setup iteration: b = 1 X0 = 0xF2E8C8B1, X1 = 0x38E06FA7, X2 = 0x9A0D72C0, X3 = 0xF
21F5334, X4 = 0xCACDCCC3, X5 = 0x4B239CBE, X6 = 0x0565DCCC, X7 = 0xB 1587C8D, C0 = 0x8433018A, C1 = 0xAF9E97C4, C2 = 0x47FCDE5D, C3 = 0x8 9310A4B, C4 = 0x96FA1124, C5 = 0x6310605E, C6 = 0xB0260F49, C7 = 0x6 475F87FInner state after fourth key setup iteration: b = 0 X0 = 0x1D059312, X1 = 0xBDDC3E45, X2 = 0xF440927D, X3 = 0x5
0CBB553, X4 = 0x36709423, X5 = 0x0B6F0711, X6 = 0x3ADA3A7B, X7 = 0xE B9800C8, C0 = 0x6BD17B74, C1 = 0x2986363E, C2 = 0xE676C5FC, C3 = 0x7 0CF8432, C4 = 0x10E1AF9E, C5 = 0x018A47FD, C6 = 0x97C48931, C7 = 0xD E5D96F9Inner state after final key setup xor: b = 0 X0 = 0x1D059312, X1 = 0xBDDC3E45, X2 = 0xF440927D, X3 = 0x5
0CBB553, X4 = 0x36709423, X5 = 0x0B6F0711, X6 = 0x3ADA3A7B, X7 = 0xE B9800C8, C0 = 0x5DA1EF57, C1 = 0x22E9312F, C2 = 0xDCACFF87, C3 = 0x9 B5784FA, C4 = 0x0DE43C8C, C5 = 0xBC5679B8, C6 = 0x63841B4C, C7 = 0x8 E9623AAInner state after generation of 48 bytes of output: b = 1 X0 = 0xB5428566, X1 = 0xA2593617, X2 = 0xFF5578DE, X3 = 0x7
293950F, X4 = 0x145CE109, X5 = 0xC93875B0, X6 = 0xD34306E0, X7 = 0x4 3FEEF87, C0 = 0x45406940, C1 = 0x9CD0CFA9, C2 = 0x7B26E725, C3 = 0x8 2F5FEE2, C4 = 0x87CBDB06, C5 = 0x5AD06156, C6 = 0x4B229534, C7 = 0x0 87DC224The 48 output bytes: S[0] = [3D 2D F3 C8 3E F6 27 A1 E9 7F C3 84 87 E2 51 9C] S[1] = [F5 76 CD 61 F4 40 5B 88 96 BF 53 AA 85 54 FC 19] S[2] = [E5 54 74 73 FB DB 43 50 8A E5 3B 20 20 4D 4C 5E]
B.2. Testing the IV Setup
key = [91 28 13 29 2E ED 36 FE 3B FC 62 F1 DC 51 C3 AC] iv = [C3 73 F5 75 C1 26 7E 59]
Inner state during key setup: as above
Inner state after IV expansion: b = 0 X0 = 0x1D059312, X1 = 0xBDDC3E45, X2 = 0xF440927D, X3 = 0x5
0CBB553, X4 = 0x36709423, X5 = 0x0B6F0711, X6 = 0x3ADA3A7B, X7 = 0xE B9800C8, C0 = 0x9C87910E, C1 = 0xE19AF009, C2 = 0x1FDF0AF2, C3 = 0x6 E22FAA3, C4 = 0xCCC242D5, C5 = 0x7F25B89E, C6 = 0xA0F7EE39, C7 = 0x7 BE35DF3Inner state after first IV setup iteration: b = 1 X0 = 0xC4FF831A, X1 = 0xEF5CD094, X2 = 0xC5933855, X3 = 0xC
05A5C03, X4 = 0x4A50522F, X5 = 0xDF487BE4, X6 = 0xA45FA013, X7 = 0x0 5531179, C0 = 0xE9BC645B, C1 = 0xB4E824DC, C2 = 0x54B25827, C3 = 0xB B57CDF0, C4 = 0xA00F77A8, C5 = 0xB3F905D3, C6 = 0xEE2CC186, C7 = 0x4 F3092C6Inner state after fourth IV setup iteration: b = 1 X0 = 0x6274E424, X1 = 0xE14CE120, X2 = 0xDA8739D9, X3 = 0x6
5E0402D, X4 = 0xD1281D10, X5 = 0xBD435BAA, X6 = 0x4E9E7A02, X7 = 0x9 B467ABD, C0 = 0xD15ADE44, C1 = 0x2ECFC356, C2 = 0xF32C3FC6, C3 = 0xA 2F647D7, C4 = 0x19F71622, C5 = 0x5272ED72, C6 = 0xD5CB3B6E, C7 = 0xC 9183140 ========================= ========================= ========================= ==
Da feits vom Boa weg.
... and I don't really think your English is up to the fine distinction between conformance testing and mathematical proof...
Thomas Prufer
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
verifizierten Libraries linkt und auf einer mit verifizierter Firmware
Und _DAS_ ist ein Beschaffungsproblem.
Marc
beschaffen.
Gerrit
Am 31.03.2022 um 12:59 schrieb Marc Haber:
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
tet
between
durch
(eigentlich)
|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 I Vs |will lead to unique keystreams.
auf der Zielhardware. Damit werden auch Compiler-Bugs erwischt und auch eventuelle CPU-Bugs.
Am 31.03.22 um 12:59 schrieb Marc Haber:
Geht so - inzwischen gibt es da schon ein paar Dinge.
Gesamtsystems braucht, aber wenn der Scope nur die Verifikation des Codes ist, kann man die Korrektheit des Rests einfach voraussetzen. An
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
Formale Verifikation macht man am Schreibtisch.
Seltsam ... tut sie nicht.
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*.nicht korrekt ist.
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
Oder ob in der Hardware eine Backdoor eingebaut wurde.
Volker
Begriffe.
formale Verifikation eher nicht die Regel.
einhergehenden Schwierigkeiten nicht eingesehen wurden, von denen eine bei der DIY-Implementierung von kryptografischen Algorithmen typischerweise die
Und "falsch implementiert" darf gerne dehnbarer interpretiert werden. Schellong erlaubt ja keinen Code-Review, daher kann von "nach allen Regeln
und in die Jahre gekommen" bis hin zu "unwartbar schlampig hingerotzt" und
Volker
Have something to add? Share your thoughts — no account required.
Ask the community — no account required