Je pravda, že zpravodajství o bezpečnosti je poněkud jednotvárné. Jedna díra na druhé. Na druhé straně od počítače
* připojeného k celosvětové síti,
* provozovaného na komplikovaném operačním systému a
* umožnujícího uživatelům dělat, co je napadne,
se nic jiného očekávat nedá. A je jedno jaký počítač a jaký operační systém to je.
Ono je to jeste horsi. Vem si takove seL4 jadro. Maji matematicky dukaz, ze je nehacknutelne. Ale uz pred lety tam byl dodatek, ze nehacknutelne za predpokladu bezchybne MMU jednotky. Jako by nekdo neco vedel nebo alespon tusil. A pak prisla smrst chyb ohledne postranich kanalu nejen u Intelu a ve vysledku je system jako celek deravy take.
SEL4 je formálně verifikované. To lze ale vždy jen za určitých předpokladů, nelze formálně verifikovat kompletně celý systém, stejně jako nelze mít matematický model než axiomů. Bezchybnou MMU tam nikdo explicitně nezmínil, zmíněna byla bezchybná implementace HW instrukcí (kam spadá i MMU) a absence postranních kanálů (kam spadá i Spectre).
Android je designovaný jako jedna velká díra. Má dvě funkce - udržet uživatele a leaknout maximální množství privátních dat, které ještě projde přes zákony, takovýmn způsobem, aby z toho měl Google zisk, tečka. Ostaně se podívejme, od koho si vzal s win10 Microsoft příklad a zavedl do systému padesát různých špionů.