20 Oct
2015
20 Oct
'15
1:47 p.m.
Příklad programu, který nemusí být open-source, a přitom o něm lze dokázat, že soukromí ctí: https://sel4.systems/
Sorry, jejich dokazovač potřebuje vidět zdroják.
Dokazovač, který to uvaří přímo ze zkompilovaného kódu, si implementujte za domácí úkol ;)
:-)) Stejne bys potreboval videt specifikaci, coz je takovej metazdrojak, abys vedel co vlastne mas dokazovat. Ale asi by slo ten dukaz preformulovat tak aby se tykal primo strojoveho kodu. Ale ta jednoducha cesta ktera me napada by umoznovala rekonstruovat Cckovy zdrojak z toho dukazu.