AK <n...@n...com> wrote:
> U?ytkownik "Waldek Hebisch" <a...@m...uni.wroc.pl> napisa?:
>
> > Z innej beczki, kilka lat temu zweryfikowano
> > formalnie mikrojado L4.
>
> Nie wierz?. C nie nadaje sie do weryfikacji formalnej poprawnosci programow
> w nim pisanych (chyba ze jest to baaardzo okrojone C - i to o wiele bardziej niz
Misra C),
> a jadro to jaderko na przyslowiowych "kilku kartkach" i "specjalnie pisane" pod
werfyfikacj?.
>
> W zwyklym C/C++ formalna weryfikacja pooprawnosci to zwykla
> uluda (i taka na zawsze zostanie).
>

Mikrojado L4 ma kolo 8000 lini kodu. Sa ograniczenia na to co sie
weryfikuje i na jezyk. ZCW weryfikacja obemuje np. sprawdzenie ze
nie ma przepelnien buforow. We efekci dostajesz z szukoscia
oczekiwana od C i najlepszym bezpieczenstwem jakie dzis daje
jakakolwiek techmika programowa. Kod L4 jest dostepny na sieci.
Za dokumentacje weryfikacji trzeba zaplacic grupa forse, wiec
ta czesc musisz przyjac na wiare,

A propo, Microsoft twierdzi ze maja lepsze metody i potrafia
zweryfikowac wieksze programy. Do calego Windowsa to daleko
(trzeba by milony linii), ale chca zwerufikwac kawalek
majacy kolo 60 tys. linii. Ostatnia wiadomosc jaka slyszalem
(rok czy dwa lata temu) ze zweryfkowali kolo 30 tys. linii.
Kod byl wczesnij napisany i ponoc jak sie cos nie chce
werifikowac to w kodzie poprawiaja tylko bugi, a przeciwnym
razie poprawija narzedzia.

Co do C to jest rozpracowana odpowiednia logika i ponoc teraz
nie sprawia wiecej problemow niz inne jezyki. Zeby bylo
jasne, weryfikcja polega na dodaniu (recznym) annotacji
i potem poprawnosc logiczna calosci sprawdza maszyna.
L4 wymagal cos kolo 8 linii annotacji na linie kodu.
Microsoft twierdzi ze przy ich metodzie wystarcza
kolo 1 lini annotacji na linie kodu. Na razie pisanie
annotacji wymaga duzo pracy i potrzeba do tego
kwalifikacji. Nie zmienia to faktu ze w przeszlosci
w mozna bylo tylko marzyc o weryfikacji na taka
skale.

Jesli interesuje Cie weryfikacja to mozesz popatrzyc na
pojekt CompCert:

compcert.inria.fr

Tam bierze sie normalny komilator C i weryfikje sie ze
kod maszynowy jest poprawnym tlumaczeniem zrodla.


--
Waldek Hebisch
h...@m...uni.wroc.pl