2 ms·
Formal verification is a thing. Good architectures make undesirable action rare. What's the last time you heard about a worm that spreads from one Android phone
by flangola7 4y ago
Formal verification is a thing. Good architectures make undesirable action rare. What's the last time you heard about a worm that spreads from one Android phone to the next, without the owners realizing it?
- mavhc 4y agoGiven that the majority of android phones have dozens of well known security flaws (because they don't get updates, or get them very late), it's kinda weird they're not all one massive botnet. Why is that?
- flangola7 4y agoMostly because the underlying design makes that difficult. On a traditional desktop an application running as root can do anything, and one running as user can do slightly less than everything. On Android running as root doesn't even exist as a function, and running as user comes with significant limitations enforced structurally by low level SELinux code in the kernel and OS. Android malware can't infect an existing application because the OS both segregates their storage and verifies code signatures. TPMs take this a step further and create not only logical but physical separation between the main CPU and many cryptographic functions. Exploits still happen but you need a much longer chain of vulnerabilities to pull it off.
- mort96 4y agoAre you claiming the entirety of Android is formally verified? Do you have links to those papers?
- flangola7 4y agoNo, I'm claiming Android has good architecture. If you combined good arch with verification then exploits would be very rare indeed.