Czy można sprawdzić poprawność programu nie uruchamiając go?

Nie bardzo rozumiem. Nie da się, ktoś spojrzy na ten kod i znajdzie ten błąd po wybuchu :)

Ale jeśli chcesz wiedzieć co się robi żeby sprawdzić poprawność, a nie jak uniknąć odpowiedzialnosci to (pytałeś o sterowanie magnesami w LHC to masz):
https://cds.cern.ch/record/2213507/files/wepgf092.pdf
http://digibuo.uniovi.es/dspace/bitstream/10651/36750/1/CERN-ACC-2014-0221.pdf
https://link.springer.com/content/pdf/10.1007/978-3-662-43613-4_18.pdf

Koledze chyba chodzi o to, że nie da się sprawdzić continuum wszystkich przypadków. Wystarczy, że przetestujesz kilka przypadków należących do tej samej klasy równoważności i warunki brzegowe. Wtedy uznajesz, że program działa dla całego continuum.

Innymi słowy wyobraź sobie, że masz unit test dla funkcji, która przyjmuje wartości od 1 do 100, ale jako float. Znając rozmiar floata teoretycznie jesteś w stanie przebadać wszystkie przypadki, jednak w praktyce wystarczy sprawdzić test dla kilku losowych wartości z tego przedziału, z brzegu i upewnić się, że funkcja zareaguje poprawnie, jeśli dostanie argument z poza dziedziny.

Kojarzy mi się cytat Donalda Knutha: "Beware of bugs in the above code; I have only proved it correct, not tried it". W przeciwieństwie do abstrakcji jaką jest matematyka, kod działa w rzeczywistym, z definicji niedoskonałym świecie. Najprostszy nawet program pokroju sprawdzenia, czy x jest większe od 10 może zawieść. Musimy poczynić po drodze wiele założeń i zaufać wielu elementom - tak kompilatorowi (że poprawnie przetłumaczy kod na instrukcje procesora) jak i hardware'owi (że je faktycznie poprawnie wykona). Co jeżeli sprzęt po prostu zużyje się po X latach użytkowania lub zostanie uszkodzony nagłym skokiem napięcia? Co jeżeli jakaś losowa wiązka promieniowania kosmicznego akurat trafi w hardware i spowoduje, że zgubi się jakiś bit...? (to wbrew pozorom rzeczywisty problem). Nawet zatem gdyby można było przetestować kod dla każdej możliwej kombinacji danych dalej może nastąpić sytuacja, że z przyczyn zewnętrznych kod zawiedzie. Może również zawieść ponieważ jakiś hacker podsunie celowo tak spreparowane dane, żeby dokonać różnych szkód - słynna jest tu historia uszkodzenia irańskich reaktorów wirusem komputerowym (Stuxnet). Tak że nie, nie da się uzyskać 100% poprawności, można jedynie do niej dążyć.

Oczywiście, że się da. Po pierwsze nie uprawia się radosnej twórczości przy klawiaturze (a tak dziś wygląda programowanie w większości przypadków) tylko pisze się zgodnie ze skrupulatnie zaprojektowanym wcześniej algorytmem, który zweryfikowany jest nie tylko poprzez testy ale także pod kątem analitycznym, złożoności itd. Poza tym są różnego rodzaju symulatory, emulatory, środowiska testowe, których zadaniem jest przetestowanie programu jako całości. Ale generalnie jest to trudne.

Testy są różnego poziomu.

Property based testy podnoszą nieco szanse poprawności.
Testowanie mutacyjne wyłapuje potencjalne luki w testach (i czasem dość betonuje soft - broń obosieczna).

Następnym etapem jest type level programming - tu już można dojść blisko tego co daje weryfikacja formalna (która jest po prostu za droga do powszechnego użycia).
Ale nie dość, że wymaga to odpowiedniego języka, to jeszcze praktyczne jest tylko w części zastosowań - logiki związanej z obliczenami tak raczej nie przetestujesz.

Ostatecznie możesz nawet użyć języka typu Agda, w którym musisz przekonać kompilator co do tego, że masz rację :-)
Problem taki, że Agda nie jest już Turing Complete i mimo, że zaskakująco dużo rzeczy da się zrobić - to z definicji nie wszystko.

Bardziej chodzi mi o to czy da się wybronić logikę programu która mimo praktycznie 100% coverage co jakiś czas generuje total system failure idący w miliony dolców. Nie znamy powodu błędu - ale jednak on występuje. Czy da się stwierdzić autorytatywnie - nasz kod jest w porządku, błąd tkwi gdzieś indziej?

Spearhead napisał(a):

Kojarzy mi się cytat Donalda Knutha: "Beware of bugs in the above code; I have only proved it correct, not tried it".

Ale to już jest gigantyczny sukces! Przesuwamy odpowiedzialność z naszego kodu na hardware który go wykonuje. Unit testy to w zasadzie tautologia, jeśli w hardware jest błąd, nic nam nie dają w dłuższej perspektywie.

Czy da się stwierdzić autorytatywnie - nasz kod jest w porządku, błąd tkwi gdzieś indziej?

Jasne, jak znajdziesz przyczynę problemu i pokażesz ze znajduje sie ona poza kodem :)

Praktycznie na to masz to jest log diagnostyczny:-(
Można wrzucać co się da (jeśli nie jest problemem np. ochrona danych),
potem w razie problemu możemy wykazać, że jeśli hardware działał dobrze to nie mogły się pojawić takie i takie wartości.
Miałem raz akcję : błąd w jvm/od (jvm niedostosowany do wchodzącego kernela 2.4), raz obfuskowany kod zewnętrznej biblioteki żle działał na nowszym jvm i dzięki logom można to było wykryć i zdiagnozować.

https://en.wikipedia.org/wiki/Formal_verification

A jednak się da! Ponoć nawet twórcy hardware z tego intensywnie korzystają by przerzucić winę na biednych software devów. Nam zostaje się tłumaczyć :(

loza_wykletych napisał(a):

https://en.wikipedia.org/wiki/Formal_verification

A jednak się da! Ponoć nawet twórcy hardware z tego intensywnie korzystają by przerzucić winę na biednych software devów. Nam zostaje się tłumaczyć :(

Weryfikacja formalna, Święty Graal Dijkstra. Niestety weryfikacja formalna jest kosztowna i normalne języki programowania tego nie wspierają, tylko eksperymentalne języki używane przez matematyków. Może za 20 lat to się zmieni, a może nigdy :(
Dziś to nawet Haskella ludzie uważają za dziwnego i trudnego, a Haskell nie jest celem tylko jednym z etapów do weryfikacji formalnej

Czyli zostaje nam indukcja zamiast dedukcji? Toż to przecież katastrofa dla branży.

A formalne dowody swoich wypocin na forum też przeprowadzasz? Pewnie nie, bo ci się to nie opłaca. To właśnie rachunek zysków i kosztów decyduje o tym co się weryfikuje formalnie, a co nie.

Na tej stronie Wiki co przytoczyłeś https://en.wikipedia.org/wiki/Formal_verification jest napisane o weryfikacji oprogramowania, np:

As of 2011, several operating systems have been formally verified: NICTA's Secure Embedded L4 microkernel, sold commercially as seL4 by OK Labs;[10] OSEK/VDX based real-time operating system ORIENTAIS by East China Normal University;[citation needed] Green Hills Software's Integrity operating system;[citation needed] and SYSGO's PikeOS.[11][12]

Weryfikacja formalna ze względu na koszty ma szanse na małym fragmencie kodu, a i to przy założeniu, że masz odpowiedni język.
Np. w javie możesz kilka metod zanalizować... i przy pewnych założeniach żadne inne części systemu nie mogą wpłynąć na to co się dzieje (faktycznie mogą, ale w sposób widoczny - np..OutOfMemory errror).
Już w C/ C++ jest to więkzszy problem, bo musisz zabezpieczyć przed jechaniem po pamięci (pewnie się da, ale nie znam się na tym).

jarekr000000 napisał(a):

Weryfikacja formalna ze względu na koszty ma szanse na małym fragmencie kodu, a i to przy założeniu, że masz odpowiedni język.

No ale zaraz przecież jeśli programowanie jest czysto dedukcyjne to powinno się automatycznie weryfikować formalnie (w końcu to zbiór abstrakcyjnych regułek logicznych). Skoro powstają narzędzia zautomatyzowanej weryfikacji formalnej dla np. VHDL to co broni wdrożyć coś takiego w większości branży? No chyba że w hardware błąd logiczny jednego obwodu powoduje miliardowe straty gdzie w software który się na nim wykonuje co najwyżej dopisanie jednego unita i uśmiech do kolegów

Wibowit napisał(a):

A formalne dowody swoich wypocin na forum też przeprowadzasz? Pewnie nie, bo ci się to nie opłaca.

Sugerujesz że można przeprowadzać dowody formalne na wypowiedziach opartych o nieformalną gramatykę i leksykę? Niebezpieczna to droga młody padawanie.

Co do automatycznej weryfikacji formalnej - Turing to świnia.

No ale zaraz przecież jeśli programowanie jest czysto dedukcyjne to powinno się automatycznie weryfikować formalnie (w końcu to zbiór abstrakcyjnych regułek logicznych). Skoro powstają narzędzia zautomatyzowanej weryfikacji formalnej dla np. VHDL to co broni wdrożyć coś takiego w większości branży? No chyba że w hardware błąd logiczny jednego obwodu powoduje miliardowe straty gdzie w software który się na nim wykonuje co najwyżej dopisanie jednego unita i uśmiech do kolegów

Nie wiem co jest weryfikowane w hardware, ale istnieją kompilatory kompilujące kod OpenCL (czyli takie pseudo-C) do FPGA, czyli w pewnym sensie kompilują software do hardware. Idąc tym tropem udowadniając poprawność takiego hardware automatycznie udowadniamy też poprawność software.

Sugerujesz że można przeprowadzać dowody formalne na wypowiedziach opartych o nieformalną gramatykę i leksykę? Niebezpieczna to droga młody padawanie.

Nikt ci nie broni, by nie formalizować swojego języka, stworzyć jakiś podzbiór o sztywnych regułach albo użyć gotowca jak np https://en.wikipedia.org/wiki/Lojban To jest pewien koszt i tylko od ciebie zależy czy chcesz go ponieść.

PS:
Ponadto czasami łata się błędy w hardware za pomocą software. Dla przykładu Intel ma ostatnio bardzo dziurawe procesory (Spectre, Meltdown i przyjaciele), a więc ma błędy w hardware. Łata je mikrokodem (a więc software, a konkretniej jego podtypem czyli firmware) oraz zmianami w kompilatorach.

Może cię zainteresować Coq

Jest całkiem popularny. Byłem na warsztatach - na dłuższą metę nic z tego nie wyniosłem - za wysokie progi, ale może Ciebie zainspiruje.

Wibowit napisał(a):

Nikt ci nie broni, by nie formalizować swojego języka, stworzyć jakiś podzbiór o sztywnych regułach albo użyć gotowca jak np https://en.wikipedia.org/wiki/Lojban To jest pewien koszt i tylko od ciebie zależy czy chcesz go ponieść.

Mógłbym, ale wtedy byłbym koderem a nie artystą.

PS:
Ponadto czasami łata się błędy w hardware za pomocą software. Dla przykładu Intel ma ostatnio bardzo dziurawe procesory (Spectre, Meltdown i przyjaciele), a więc ma błędy w hardware. Łata je mikrokodem (a więc software, a konkretniej jego podtypem czyli firmware) oraz zmianami w kompilatorach.

Spekulacje chyba ciężko poddaje się jakimś dowodom. Szczególnie spekulacje na pamięci.

Na studiach bawiliśmy się trochę http://spinroot.com/spin/whatispin.html. Może Ciebie to zainteresuje. Do tego z teorii to logiki modalne, LTL itp. Narzędzia dość egzotyczne :)

Spekulacje chyba ciężko poddaje się jakimś dowodom. Szczególnie spekulacje na pamięci.

Jeśli tak to kiepski jesteś w dowodzeniu. Spekulacje są też popularne w software, np https://en.wikipedia.org/wiki/Optimistic_concurrency_control (np https://en.wikipedia.org/wiki/Software_transactional_memory ) Powiedziałbym nawet, że programowanie współbieżne w ogólności to pewnego rodzaju spekulacja.
Coraz więcej oprogramowania jest oparte o https://en.wikipedia.org/wiki/Eventual_consistency np https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type a więc masz sytuację taką, że dane pomiędzy poszczególnymi węzłami przetwarzania są rozjechane (rozbieżne między sobą), a mimo tego i tak system działa poprawnie, bo dąży do uzgodnienia wspólnej postaci danych.

Intel ma wsparcie dla transactional memory w swoich procesorach https://en.wikipedia.org/wiki/Transactional_Synchronization_Extensions ale niestety jest (albo było) zbugowane (patrz: Zombieload v2), więc i tak tego typu spekulacja jest bezpieczniejsza w software.

Weryfikacja hardware to nie tylko weryfikacja poprawności algorytmów, ale też weryfikacja timingów, długości połączeń, zakłóceń, etc Poprawność algorytmów zaimplementowanych w hardware można sprawdzić też testami jednostkowymi, np https://github.com/VUnit/vunit

Układy asynchroniczne https://en.wikipedia.org/wiki/Asynchronous_circuit mogą być szybsze niż synchroniczne, ale trudniej się je projektuje, bo są podatne na race conditions:

In asynchronous circuits, there is no clock signal, and the state of the circuit changes as soon as the inputs change. Since asynchronous circuits don't have to wait for a clock pulse to begin processing inputs, they can be faster than synchronous circuits, and their speed is theoretically limited only by the propagation delays of the logic gates. However, asynchronous circuits are more difficult to design and subject to problems not found in synchronous circuits. This is because the resulting state of an asynchronous circuit can be sensitive to the relative arrival times of inputs at gates. If transitions on two inputs arrive at almost the same time, the circuit can go into the wrong state depending on slight differences in the propagation delays of the gates. This is called a race condition. In synchronous circuits this problem is less severe because race conditions can only occur due to inputs from outside the synchronous system, called asynchronous inputs. Although some fully asynchronous digital systems have been built (see below), today asynchronous circuits are typically used in a few critical parts of otherwise synchronous systems where speed is at a premium, such as signal processing circuits.

Spearhead napisał(a):

Kojarzy mi się cytat Donalda Knutha: "Beware of bugs in the above code; I have only proved it correct, not tried it". W przeciwieństwie do abstrakcji jaką jest matematyka, kod działa w rzeczywistym, z definicji niedoskonałym świecie. Najprostszy nawet program pokroju sprawdzenia, czy x jest większe od 10 może zawieść. Musimy poczynić po drodze wiele założeń i zaufać wielu elementom - tak kompilatorowi (że poprawnie przetłumaczy kod na instrukcje procesora) jak i hardware'owi (że je faktycznie poprawnie wykona). Co jeżeli sprzęt po prostu zużyje się po X latach użytkowania lub zostanie uszkodzony nagłym skokiem napięcia? Co jeżeli jakaś losowa wiązka promieniowania kosmicznego akurat trafi w hardware i spowoduje, że zgubi się jakiś bit...? (to wbrew pozorom rzeczywisty problem). Nawet zatem gdyby można było przetestować kod dla każdej możliwej kombinacji danych dalej może nastąpić sytuacja, że z przyczyn zewnętrznych kod zawiedzie. Może również zawieść ponieważ jakiś hacker podsunie celowo tak spreparowane dane, żeby dokonać różnych szkód - słynna jest tu historia uszkodzenia irańskich reaktorów wirusem komputerowym (Stuxnet). Tak że nie, nie da się uzyskać 100% poprawności, można jedynie do niej dążyć.

Ale to nie są bugi programu. W takim Sel4 też masz wyjustowane, że program będzie działał poprawnie jeżeli instrukcje procesora działają tak jak w dokumentacji, hardware jest nieuszkodzony etc.

https://sel4.systems/Info/FAQ/proof.pml

What we assume
With a proof in formal logic, it is important to understand what its basic assumptions are, because this is where fault can still occur. Our proof about the seL4 microkernel goes down to the level of the binary code.

Assembly: the seL4 kernel, like all operating system kernels, contains some assembly code, about 340 lines of ARM assembly in our case. For seL4, this concerns mainly entry to and exit from the kernel, as well as direct hardware accesses. For the proof, we assume this code is correct.
Hardware: we assume the hardware works correctly. In practice, this means the hardware is assumed not to be tampered with, and working according to specification. It also means, it must be run within its operating conditions.
Hardware management: the proof makes only the most minimal assumptions on the underlying hardware. It abstracts from cache consistency, cache colouring and TLB (translation lookaside buffer) management. The proof assumes these functions are implemented correctly in the assembly layer mentioned above and that the hardware works as advertised. The proof also assumes that especially these three hardware management functions do not have any effect on the behaviour of the kernel. This is true if they are used correctly.
Boot code: the proof currently is about the operation of the kernel after it has been loaded correctly into memory and brought into a consistent, minimal initial state. This leaves out about 1,200 lines of the code base that a kernel programmer would usually consider to be part of the kernel.
Virtual memory: under the standard of 'normal' formal verification projects, virtual memory does not need to be considered an assumption of this proof. However, the degree of assurance is lower than for other parts of our proof where we reason from first principle. In more detail, virtual memory is the hardware mechanism that the kernel uses to protect itself from user programs and user programs from each other. This part is fully verified. However, virtual memory introduces a complication, because it can affect how the kernel itself accesses memory. Our execution model assumes a certain standard behaviour of memory while the kernel executes, and we justify this assumption by proving the necessary conditions on kernel behaviour. The thing is: you have to trust us that we got all necessary conditions and that we got them right. Our machine-checked proof doesn't force us to be complete at this point. In short, in this part of the proof, unlike the other parts, there is potential for human error.
DMA: we assume that the CPU and MMU are the only devices that access memory directly. The proof can correctly ignore memory-mapped registers of devices, but has to assume that DMA devices are either not present or do not misbehave, for instance by overwriting the kernel. In practise this means, that while normal user-level drivers cannot break kernel security, drivers for DMA enabled devices can and must be formally verified for the proof to carry over. We have current work underway to eliminate this assumption using the SystemMMU on ARM.
Information side-channels: this assumption applies to the confidentiality proof only and is not present for functional correctness or integrity. The assumption is that the binary-level model of the hardware captures all relevant information channels. We know this not to be the case. This is not a problem for the validity of the confidentiality proof, but means that its conclusion (that secrets do not leak) holds only for the channels visible in the model. This is a standard situation in information flow proofs: they can never be absolute. As mentioned above, in practice the proof covers all in-kernel storage channels but does not cover timing channels

Wibowit napisał(a):

Weryfikacja hardware to nie tylko weryfikacja poprawności algorytmów, ale też weryfikacja timingów, długości połączeń, zakłóceń, etc Poprawność algorytmów zaimplementowanych w hardware można sprawdzić też testami jednostkowymi, np https://github.com/VUnit/vunit

Jest pewna różnica gdy algorytm formalnie niepoprawny uruchomiony daje poprawne wyniki a odwrotnością. W pierwszym przypadku możemy łatwo założyć że skoro działa to dobrze mimo że działanie jest side-produktem czegoś innego.

I ty cały czas piszesz o modelach co do których nawet są prace że owszem - matematycznie pięknie wyglądają, implementacyjnie działają ale formalna analiza ich implementacji jest nietrywialna - https://hal.inria.fr/hal-01398007/document

I ty cały czas piszesz o modelach co do których nawet są prace że owszem - matematycznie pięknie wyglądają, implementacyjnie działają ale formalna analiza ich implementacji jest nietrywialna - https://hal.inria.fr/hal-01398007/document

Coś puenty zabrakło, bo nie wiem do czego się odnieść. Owszem są rzeczy prostsze do zrobienia i trudniejsze. Formalna weryfikacja jest na tyle trudna, że robi się ją tylko w specyficznych przypadkach, a jak widać w przypadku np procków Intela to i czasami Intel przyoszczędzi na testach. Jak chcesz przykłady błędów w hardware, które nie wymagają spekulacji to proszę bardzo:

• https://en.wikipedia.org/wiki/Pentium_FDIV_bug
• https://en.wikipedia.org/wiki/MOS_Technology_6502#Bugs_and_quirks

Weź pod uwagę to, że dzisiejsze skomplikowane układy składają się z identycznych klocków, np X-rdzeniowy procesor składa się zwykle z jednego projektu rdzenia (czasami dwóch, w bardzo sporadycznych przypadkach więcej) powielonego X razy. Stąd możesz dowieść poprawność raz. Projektowanie takiego rdzenia dzisiaj idzie w setki milionów dolarów i to dla jednej wersji. Kolejne generacje procesorów to kolejny wydatek i to mimo iż nie są przepisywane totalnie od zera, a są ewolucją poprzednich wersji.

Innymi słowy: jeśli masz budżet na formalną weryfikację hardware czy software i znajdzie się chętny na wykonanie takiego zadania to wykładasz hajs i masz zweryfikowane :) Nie ma tu żadnej filozofii.

Wibowit napisał(a):

Innymi słowy: jeśli masz budżet na formalną weryfikację hardware czy software i znajdzie się chętny na wykonanie takiego zadania to wykładasz hajs i masz zweryfikowane :) Nie ma tu żadnej filozofii.

A nie bardziej o to że wykonanie prototypu układu to już tysiące dolarów a już całej matrycy do naświetlań to już dziesiątki milionów? Więc w zasadzie nie masz na czym testować.

A nie bardziej o to że wykonanie prototypu układu to już tysiące dolarów a już całej matrycy do naświetlań to już dziesiątki milionów? Więc w zasadzie nie masz na czym testować.

Coś ci się skale pomyliły.
https://semiengineering.com/racing-to-107nm/

For those who migrate beyond 16nm/14nm, it will require deep pockets. In total, it will cost $271 million to design a 7nm chip, according to Gartner. In comparison, it costs around $80 million to design a 16nm/14nm chip and $30 million for a 28nm planar device, the research firm said.

https://www.extremetech.com/computing/272096-3nm-process-node

Spearhead napisał(a):

Nawet zatem gdyby można było przetestować kod dla każdej możliwej kombinacji danych dalej może nastąpić sytuacja, że z przyczyn zewnętrznych kod zawiedzie. Może również zawieść ponieważ jakiś hacker podsunie celowo tak spreparowane dane, żeby dokonać różnych szkód

Tak mi się przypomniało:

pracownicy Uniwersytetu Waszyngtona w Seattle, którym udało się** wszczepić w próbkę DNA kod złośliwego oprogramowania i za jego pomocą przejąć komputer, który analizował ów materiał genetyczny**. Zadanie nie było oczywiście łatwe. Prowadzący projekt naukowcy wielokrotnie przepisywali kod swojego malware'u, tak aby mógł przetrwać transformację z kodu DNA do specjalnego, cyfrowego formatu, który następnie zostaje odczytany przez komputer analizujący próbkę. Ostatecznie ich próba zakończyła się jednak sukcesem - kod został udanie "przetrawiony" przez komputer i umożliwił przejęcie nad nim kontroli.

https://www.komputerswiat.pl/aktualnosci/wydarzenia/amerykanscy-naukowcy-zhakowali-komputer-za-pomoca-kodu-dna/sr3qm3t