J
Josef Moellers
Guest
On 29.03.22 15:14, Helmut Schellong 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.
Nein, ich will ihnen nicht widersprechen, daà dies Test Vektoren für das
\"conformance testing\" sind. So ein Test *beweist* eben NICHT die
Korrektheit eines Codes sondern nur, daà dieser gewissen Standards
entspricht:
https://www.techtarget.com/searchsoftwarequality/definition/conformance-testing
Da steht nix von \"correctness\" sondern nur \"meets a defined set of
standards\".
Auch der Wikipedia-Artikel
https://en.wikipedia.org/wiki/Conformance_testing sprint nicht von
\"correctness\" sondern nur von \"performs according to its specified
standards.\".
Wie gesagt/geschrieben: Man kann mit einem noch so guten Test nicht die
Korrektheit *beweisen\". Man kann sein vertrauen darin durch immer
längeres Test immer weiter vergröÃern, eine 100% Sicherheit gibt kein Test!
Durch das hinzufügen von noch mehr Tests wirst Du Dich dem Ziel \"100%
Korrektheit bewiesen\" ständig asymptotisch annähern, es aber nie erreichen.
Im Wikipedia-Artikel zu \"Software Testing\" steht auch genau drin:
\"understand the risks of software implementation.\" und weiter \"Software
testing can provide objective, independent information about the quality
of software and risk of its failure to users or sponsors\" Da steht also
eindeutig, daà es Risiken gibt (mir fällt kein anderes Risiko ein als
daà der Code Fehler enthält) und man kann durch Testen diese *Risiken*
erkennen und das Vertrauen erhöhen.
Ãbereinstimmung womit?
Tja, dann glaube das bitte weiter.
Das heiÃt, sie können ganz genau angeben, wie viele Tests und mit
welchen Werten sie diese Tests durchführen müssen, um die Korrektheit zu
100% zu beweisen?
Ich behaupte, daà ihnen bewuÃt ist, daà dies nicht möglich ist.
*Jeder* auf einem Computer implementierter Algorithmus ist
deterministisch. Trotzdem kann man von vielen Algorithmen z.B. nicht
einmal theoretisch beweisen, daà sie jemals enden (Halteproblem). Ergo
kann man dies und auch das Gegenteil auch durch die besten Tests nicht
beweisen.
Das beruhigt ungemein.
Tja, das würde ich gerne mit ihnen diskutieren.
Ich finde gerade keine Email-Adresse, aber das bekomme ich hin!
Wie bitte soll den durch das Testen mit von den Entwicklern vorgegebenen
Test-Vektoren bewiesen werden, daà Elemente, die NICHT in den
Test-Vektoren enthalten sind, auch die korrekten Ergebnisse liefern?
Also hast nicht Du das bewiesen, sondern die Entwickler haben das
behauptet und Du hast das nur wiedergegeben.
NB Unser Sohn ist Professor für Mathematik an der Universität in Aarhus
und ich habe ihn gerade mal (per Email) gefragt, ob er mir ggf die
Email-Adresse von Mette Vesterager, die ist am Center for Subjectivity
Research an der Uni Kopenhagen, besorgen kann. Mal gucken, was daraus wird.
Ja, dann erübrigt sich ja die Debatte mit Dir, oh Du weiser Mann.
Zwanzig Programmiersprachen ... wow! Ich erstarre in Ehrfurcht.
Ich habe 1981 angefangen zu arbeiten (damals bei der Nixdorf Computer
AG) und die Computerei ist mein Hobby. Wie viele Programmiersprachen ich
kenne ... ich habe sie nie gezählt.
Das ist ja auch völlig irrelevant! Und wenn Du 100 Programmiersprachen
könntest, so hast Du immer noch nicht begriffen, was ich sagen will: DaÃ
man mit Testen nie und nimmer die Korrektheit eines Codes beweisen kann.
Siehe hierzu auch
https://de.wikipedia.org/wiki/Korrektheit_(Informatik)
Oder die Folien hier:
https://pi4.informatik.uni-mannheim.de/pi4.data/content/courses/2005-ws/pi1/slides/pi1-5b-2006-02-02.pdf
\"Testen nur das Vertrauen in die Korrektheit eines Programms erhöhen,
nicht aber die Korrektheit beweisen.\"
Oder die Folien hier:
https://www.mathematik.uni-marburg.de/~gumm/Lehre/WS07/PraktischeInformatikI/Folien/14_Korrektheit.pdf
\"Durch Testen kann man nur Anwesenheit von
Fehlern feststellen, nicht aber ihre
Abwesenheit (E. Dijkstra)\"
Dijstra\'s Essay \"On the reliability of programs\" kannst Du übrigens hier
nachlesen:
https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD303.html
Ich zitiere mal (sinngemäÃ) einen Herrn Schellong: \"Willst Du dem
widersprechen?\"
Dijstra\'s These wird übrigens hier diskutiert:
https://blog.liw.fi/posts/2019/06/29/dijkstra_was_only_partially_correct_about_testing/
Und auch dort steht \"Tests donât tell you that code works in cases that
arenât tested. Tests tell you code works in the cases that are tested.
If you want it to work in some other case, you add a test, or expand an
existing test to cover the case youâre interested in.\"
> Ich habe u.a. die Bücher von Knuth.
Ja, die sind gut.
Was sagt Knuth denn zum Testen?
http://www.informit.com/articles/article.aspx?p=1193856
\"As to your real question, the idea of immediate compilation and \"unit
tests\" appeals to me only rarely, when Iâm feeling my way in a totally
unknown environment and need feedback about what works and what doesnât.\"
OK, es geht um \"Unit Tests\", aber auch das sind Tests und er lehnt sie ab!
Das wage ich zu bezweifeln. Schau\'n \'mer mal, ob unser Ãltester mir die
Adresse von Mette besorgen kann, dann frage ich sie.
Wie gesagt: Hybris.
Ich sage ja nicht, daà sie fehlerhaft SIND, ich behaupte nur, daà man
durch Testen niemals eine Korrektheit BEWEISen kann.
Das ist in der Informatik allgemein bekannt und akzeptiert.
Daà man trotzdem testet hat sicherlich damit zu tun, daà der
mathematisch-logische KorrektheitsBEWEIS eines nicht-trivialen Stücks
Code selber in besonderem MaÃe nicht-trivial ist und keiner sich die
Arbeit machen will. Ich habe mkich während meine Studiums mit \"weakest
precondition\"s und \"postcondition\"s \'rumschlagen dürfen. Es hat KEINEN
Spaà gemacht ...
Wie gesagt: Ich behaupt nicht, daà sie fehlerhaft SIND.
Nein, in erster Instanz werden Brücken *berechnet*. Die Statiker
*berechnen*, wie viel Beton und wie viel Armierung und sonstiges da
\'rein muÃ, damit eine Brücke mit einer bestimmten Spannweite eine
bestimmte Last aufnehmen kann. Am Ende wird, um das noch einmal zu
*verifizieren* ein Belastungstest gemacht. Aber wenn das nicht
*berechnet* ist, dann würde kein LKW-Fahrer darüber fahren wollen.
[...]
Und Du willst die (Er)-Kenntnisse der theoretischen Informatik nicht
anerkennen.
Josef
On 03/29/2022 09:39, Josef Moellers wrote:
On 28.03.22 22:29, Helmut Schellong wrote:
On 03/28/2022 20:23, Thomas Prufer wrote:
On Mon, 28 Mar 2022 15:28:20 +0200, Helmut Schellong
rip@schellong.biz> wrote:
Es ist _ganz generell_ richtig, was Du schreibst.
Du ignorierst jedoch die konkrete Praxis mit genau den Algorithmen,
um die es hier geht.
Diese hatte ich aufgelistet:
   |Die Kern-Algorithmen sind nicht selbst entwickelt.
   |Ich habe u.a. die Algorithmen Rabbit, Spritz, sha2_256, sha2_512,
   |sha3_256, sha3_512 (Keccak) in meine Shell bish implementiert.
   |Diese Algorithmen sind alle kryptographisch.
In der Implementierungsvorschrift der jeweiligen Entwickler der
Algorithmen
ist auch meist eine Testprozedur durch die Entwickler angegeben.
Diese habe ich jeweils durchgeführt!
Mit jeweils demjenigen Ergebnis, das Korrektheit beweist!
Hatte ich mehrfach gepostet - und wurde jeweils ignoriert.
Korrekter und beweiskräftiger geht es nicht!
Das wurde ignoriert weil es kein Beweis ist...
Beweis für was?
\"das Korrektheit beweist!\"
Es ist allgemein bekannt, daà man mit einem Test NIEMALS die
KORREKTHEIT sondern nur die UNKORREKTHEIT beweisen kann, nämlich wenn
der Test fehl schlägt.
Du kannst so lange Testen, wie Du willst, Du kannst 100% Testabdeckung
erreichen, aber Du wirst dadurch niemals beweisen können, daà der Test
nicht bei der nächsten Iteration fehl schlägt.
Der *Beweis* der Korrektheit eines Algorithmus oder seiner
Implementation (im Folgenden \"der Code\") ist eine nicht-triviale, in
der Regel mathematische Tätigkeit.
Es gibt tatsächlich Tests, die eine Korrektheit nicht beweisen können.
Das gilt jedoch nicht für kryptographische Algorithmen, die hier
aufgelistet sind.
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.
Diese Aussage wiederum beweist die Inkompetenz derer, die das
ignorierten.
Warum?
Es geht um den Beweis einer korrekten Implementation!
Genau, und die kannst Du NIEMALS durch einen Test BEWEISEN.
|This is a set of test vectors for conformance testing,
Die Entwickler von kryptographischen Algorithmen haben das aber ausgesagt.
Willst Du denen widersprechen?
Nein, ich will ihnen nicht widersprechen, daà dies Test Vektoren für das
\"conformance testing\" sind. So ein Test *beweist* eben NICHT die
Korrektheit eines Codes sondern nur, daà dieser gewissen Standards
entspricht:
https://www.techtarget.com/searchsoftwarequality/definition/conformance-testing
Da steht nix von \"correctness\" sondern nur \"meets a defined set of
standards\".
Auch der Wikipedia-Artikel
https://en.wikipedia.org/wiki/Conformance_testing sprint nicht von
\"correctness\" sondern nur von \"performs according to its specified
standards.\".
Wie gesagt/geschrieben: Man kann mit einem noch so guten Test nicht die
Korrektheit *beweisen\". Man kann sein vertrauen darin durch immer
längeres Test immer weiter vergröÃern, eine 100% Sicherheit gibt kein Test!
Durch das hinzufügen von noch mehr Tests wirst Du Dich dem Ziel \"100%
Korrektheit bewiesen\" ständig asymptotisch annähern, es aber nie erreichen.
Im Wikipedia-Artikel zu \"Software Testing\" steht auch genau drin:
\"understand the risks of software implementation.\" und weiter \"Software
testing can provide objective, independent information about the quality
of software and risk of its failure to users or sponsors\" Da steht also
eindeutig, daà es Risiken gibt (mir fällt kein anderes Risiko ein als
daà der Code Fehler enthält) und man kann durch Testen diese *Risiken*
erkennen und das Vertrauen erhöhen.
\'conformance\' heiÃt \'Ãbereinstimmung\'.
Wenn Test-Vektoren Ãbereinstimmung erzielen, ist eine Implementation
korrekt.
Ãbereinstimmung womit?
Deren Korrektheit ist durch eine Ãbereinstimmung _bewiesen_.
Das sagen die Entwickler aus!
Und Punkt.
Tja, dann glaube das bitte weiter.
Der ist gegeben, wenn die vorgeschriebenen Tests Ãbereinstimmung
ergaben.
Nein, dadurch ist nur gegeben, daà der Code bei der Durchführung der
vorgegebenen Berechnungen die erwarteten Ergebnisse liefert. Es ist
dadurch niche bewiesen, daà der Code bei der Durchführung anderer
Berechnungen, z.B. wenn andere Eingabeparameter vorgegeben werden,
immer noch die erwarteten Ergebnisse liefert.
Falsch.
Die Entwickler haben geeignete Tests vorgegeben, um die Korrektheit
beweisen zu können.
Die Entwickler wissen, daà wenn alle Tests Ãbereinstimmung ergeben, auch
alle weiteren
denkbaren Test-Vektoren zwangsweise Ãbereinstimmung ergeben würden.
Das heiÃt, sie können ganz genau angeben, wie viele Tests und mit
welchen Werten sie diese Tests durchführen müssen, um die Korrektheit zu
100% zu beweisen?
Ich behaupte, daà ihnen bewuÃt ist, daà dies nicht möglich ist.
Die Entwickler kennen ihre Entwicklung in dieser Hinsicht ganz genau.
SchlieÃlich sind die Algorithmen deterministisch.
*Jeder* auf einem Computer implementierter Algorithmus ist
deterministisch. Trotzdem kann man von vielen Algorithmen z.B. nicht
einmal theoretisch beweisen, daà sie jemals enden (Halteproblem). Ergo
kann man dies und auch das Gegenteil auch durch die besten Tests nicht
beweisen.
|We, the designers of Rabbit, hereby state that no hidden weaknesses have
|been inserted by us in the Rabbit algorithm.
Das beruhigt ungemein.
|The key expansion stage guarantees a one-to-one correspondence be-
|tween the key, the state and the counter, which prevents key redun-
|dancy. It also distributes the key bits in an optimal way to prepare
|for the the system iteration.
|The correctness of the code on different platforms is verified by
generating and comparing test vectors.
Tja, das würde ich gerne mit ihnen diskutieren.
Ich finde gerade keine Email-Adresse, aber das bekomme ich hin!
Es ist dann der Beweis erbracht, daà die vorgenommene Implementation
werte-mäÃig identisch mit der Referenz-Implementation der
Algorithmus-Entwickler ist.
Nochmals: Nein, es dadurch nur der Beweis erbracht, daà der Code bei
den vom Entwickler vorgegebenen Eingabedaten die erwarteten
Ausgabedaten erzeugt. Nichts anderes.
Erneut falsche Behauptung.
Beweise zur Abwechslung doch mal Deine Behauptung.
Wie bitte soll den durch das Testen mit von den Entwicklern vorgegebenen
Test-Vektoren bewiesen werden, daà Elemente, die NICHT in den
Test-Vektoren enthalten sind, auch die korrekten Ergebnisse liefern?
Ich habe meine nämlich mehrfach bewiesen, anhand der
Entwickler-Testprozeduren.
Also hast nicht Du das bewiesen, sondern die Entwickler haben das
behauptet und Du hast das nur wiedergegeben.
NB Unser Sohn ist Professor für Mathematik an der Universität in Aarhus
und ich habe ihn gerade mal (per Email) gefragt, ob er mir ggf die
Email-Adresse von Mette Vesterager, die ist am Center for Subjectivity
Research an der Uni Kopenhagen, besorgen kann. Mal gucken, was daraus wird.
\"This is a set of test vectors for conformance testing,\"
Hatte ich bereits gepostet.
\"Korrekter und beweiskräftiger geht es nicht!\" schrieb ich oben.
Reicht das nicht?
Falls nicht - was reicht denn dann?
Ein mathematischer Beweis, daà der Code korrekt ist, also nicht der
Nchweis, daà der Code bei der Eingabe einer (endlichen) Menge von
Eingabeparametern die erwarteten Ergebnisse liefert, sondern daà der
Code bei der Eingeba *aller erlaubten* Eingabeparametern die
erwarteten Ergebnisse liefern wird.
Dazu empfehle ich \"The Science of Programming\" von David Gries. Ist
schon gut abgehangen, aber imho immer noch gut.
Ich beherrsche etwa 20 Programmiersprachen mehr oder weniger gut - ein
weiteres Buch brauche ich nicht.
Ja, dann erübrigt sich ja die Debatte mit Dir, oh Du weiser Mann.
Zwanzig Programmiersprachen ... wow! Ich erstarre in Ehrfurcht.
Ich habe 1981 angefangen zu arbeiten (damals bei der Nixdorf Computer
AG) und die Computerei ist mein Hobby. Wie viele Programmiersprachen ich
kenne ... ich habe sie nie gezählt.
Das ist ja auch völlig irrelevant! Und wenn Du 100 Programmiersprachen
könntest, so hast Du immer noch nicht begriffen, was ich sagen will: DaÃ
man mit Testen nie und nimmer die Korrektheit eines Codes beweisen kann.
Siehe hierzu auch
https://de.wikipedia.org/wiki/Korrektheit_(Informatik)
Oder die Folien hier:
https://pi4.informatik.uni-mannheim.de/pi4.data/content/courses/2005-ws/pi1/slides/pi1-5b-2006-02-02.pdf
\"Testen nur das Vertrauen in die Korrektheit eines Programms erhöhen,
nicht aber die Korrektheit beweisen.\"
Oder die Folien hier:
https://www.mathematik.uni-marburg.de/~gumm/Lehre/WS07/PraktischeInformatikI/Folien/14_Korrektheit.pdf
\"Durch Testen kann man nur Anwesenheit von
Fehlern feststellen, nicht aber ihre
Abwesenheit (E. Dijkstra)\"
Dijstra\'s Essay \"On the reliability of programs\" kannst Du übrigens hier
nachlesen:
https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD303.html
Ich zitiere mal (sinngemäÃ) einen Herrn Schellong: \"Willst Du dem
widersprechen?\"
Dijstra\'s These wird übrigens hier diskutiert:
https://blog.liw.fi/posts/2019/06/29/dijkstra_was_only_partially_correct_about_testing/
Und auch dort steht \"Tests donât tell you that code works in cases that
arenât tested. Tests tell you code works in the cases that are tested.
If you want it to work in some other case, you add a test, or expand an
existing test to cover the case youâre interested in.\"
> Ich habe u.a. die Bücher von Knuth.
Ja, die sind gut.
Was sagt Knuth denn zum Testen?
http://www.informit.com/articles/article.aspx?p=1193856
\"As to your real question, the idea of immediate compilation and \"unit
tests\" appeals to me only rarely, when Iâm feeling my way in a totally
unknown environment and need feedback about what works and what doesnât.\"
OK, es geht um \"Unit Tests\", aber auch das sind Tests und er lehnt sie ab!
Ein mathematischer Beweis ist bei allen Algorithmen des Kontextes
prinzipiell unmöglich.
Fehler werden gegebenenfalls lange Zeit nach Veröffentlichung des Algo
von untersuchenden Experten mitgeteilt.
Die _Entwickler_ wissen, daà wenn alle Tests Ãbereinstimmung ergeben,
auch alle weiteren
denkbaren Test-Vektoren zwangsweise Ãbereinstimmung ergeben würden. (s.o.)
Das wage ich zu bezweifeln. Schau\'n \'mer mal, ob unser Ãltester mir die
Adresse von Mette besorgen kann, dann frage ich sie.
Wir befinden uns nun im Bereich der Haarspalterei, des Unsinns, des
Irrsinns.
Nein, wir befinden uns hier im Bereich der Hybris.
Falsch.
Ich bin ganz konkret praxisbezogen ziemlich kenntnisreich auf diesem
Gebiet.
Wie gesagt: Hybris.
Es ist extrem gefährlich zu behaupten, ein Code sei \"bewiesenermaÃen
korrekt, weil er gewisse Tests erfolgreich durchlaufen hat\",
insbesondere wenn es sich um sicherheitsrelevanten Code handelt.
Alle genannten Algorithmen wurden und werden weltweit millionenfach
korrekt implementiert
und konkret hunderte-millionenfach in sicherheitsfordernder Umgebung
verwendet.
Ich sage ja nicht, daà sie fehlerhaft SIND, ich behaupte nur, daà man
durch Testen niemals eine Korrektheit BEWEISen kann.
Das ist in der Informatik allgemein bekannt und akzeptiert.
Daà man trotzdem testet hat sicherlich damit zu tun, daà der
mathematisch-logische KorrektheitsBEWEIS eines nicht-trivialen Stücks
Code selber in besonderem MaÃe nicht-trivial ist und keiner sich die
Arbeit machen will. Ich habe mkich während meine Studiums mit \"weakest
precondition\"s und \"postcondition\"s \'rumschlagen dürfen. Es hat KEINEN
Spaà gemacht ...
MD5 und RC4 werden trotz Korrumpierung vor vielen Jahren weiterhin
verwendet.
Wie gesagt: Ich behaupt nicht, daà sie fehlerhaft SIND.
Ich stelle mir gerade vor, wie das ist, wenn eine Brücke als
\"bewiesenermaÃen korrekt gebaut\" ist und für den allgemeinen Verkehr
freigegeben wird, weil man nach dem Bau ein paar LKW darüber hat
fahren lassen.
So wird das seit vielleicht 150 Jahren weltweit getan.
Nein, in erster Instanz werden Brücken *berechnet*. Die Statiker
*berechnen*, wie viel Beton und wie viel Armierung und sonstiges da
\'rein muÃ, damit eine Brücke mit einer bestimmten Spannweite eine
bestimmte Last aufnehmen kann. Am Ende wird, um das noch einmal zu
*verifizieren* ein Belastungstest gemacht. Aber wenn das nicht
*berechnet* ist, dann würde kein LKW-Fahrer darüber fahren wollen.
[...]
Du willst die Kenntnisse der Entwickler und Gepflogenheiten im Bereich
der kryptographischen Cipher offensichtlich nicht anerkennen.
Und Du willst die (Er)-Kenntnisse der theoretischen Informatik nicht
anerkennen.
Josef