Lze bezpečnost softwaru dokázat matematicky?
Lze u softwarového kódu formálně dokázat jeho bezpečnost, tj. že vždy funguje pouze tak, jak jeho tvůrci zamýšleli? Protože software je v podstatě „matematika“, neměly by rigoróznímu důkazu stát v cestě žádné principiální překážky. Tým výzkumníku alespoň tvrdí, že právě tohle se mu podařilo prokázat u nově vyvinutého jádra (kernelu). Základ tohoto operačního systému obsahuje […]
Sdílet
Lze u softwarového kódu formálně dokázat jeho bezpečnost, tj. že vždy funguje pouze tak, jak jeho tvůrci zamýšleli? Protože software je v podstatě „matematika“, neměly by rigoróznímu důkazu stát v cestě žádné principiální překážky.
Tým výzkumníku alespoň tvrdí, že právě tohle se mu podařilo prokázat u nově vyvinutého jádra (kernelu). Základ tohoto operačního systému obsahuje 7 500 řádek kódu, tj. jen minimum potřebné pro komunikaci mezi hardwarem a aplikacemi. Nicméně toto jádro by se prý mohlo stát i základem prakticky použitelného operačního systému, který by se pro určité účely navíc mohl vykázat příslušným „certifikátem“.
Samotná metoda by se navíc mohla uplatnit i při analýze kódu jader dnešních nejrozšířenějších systémů (alespoň pokud by u delšího kódu šla provést v reálném čase).
Podrobnosti přináší článek na SecurityWorldu.
Komentáře
Napsat vlastní komentář
Pro přidání příspěvku do diskuze se prosím přihlašte v pravém horním rohu, nebo se prosím nejprve registrujte.