No jasne, zavisi na zvolenych kriteriach, ale ak to chapem spravne, tak urcite vlastnosti kodu/platformy su formalne dokazane (co nezarucuje uplnu nepriestrelnost). Obecne ide o to, ze dokazat bezpecnost niecoho je takmer nemozne hlavne kvoli tomu, ze nie je obecne mozne popisat vsetky vlastnosti, ktore by to malo splnovat tak, aby ziadna vlastnost neostala nepopisana (v danej logike nerozhodnutelne problemy).
Napr. existuju protokoly, ktore su dokazatelne bezpecne via BAN/GNY logiku, lenze je ich mozne napadnut sposobmi, ake tie logiky (modely) nepripustaju (nepoznaju). Napr. side channels.
Názor ke zprávičce MS Windows Home Server poškozuje soubory
