Ask HN: How do you trust that your personal machine is not compromised?

In the case of seL4, don't confuse formal verification with security. The code matches the spec, and security properties can be extracted very precisely, but spec might contain oversights/bugs which would allow an attacker to perform unexpected behaviors.

If you define security as a "lack of exploitable bugs", then security can never be proven, because it's impossible to prove a negative. Also many formally verified systems have had critical bugs discovered, like the KRACK attacks in WPA. The formal verification wasn't wrong, just incomplete, because modeling complex systems is inherently an intractable problem.

The fact that seL4 doesn't even offer bug bounties should be a huge red flag that this is still very much an academic exercise, and should not be used in places where security actually matters.

https://github.com/seL4/seL4/blob/master/SECURITY.md

Before defining any strategy, you need to define an appropriate threat model. Which kind of information are you storing on your device and who can target you?

If you are a standard person and not doing any illegal, the information that you need to protect are mostly related to financial and personal standpoint. So you need to protect you bank/credit card/cryptowallet with encryption and/or MFA. For financial information, use the same criteria, according also to level of continentality that you want to achieve: it's stupid to encrypt your cat pictures, it may be worth to encrypt cipher your son pictures, it's mandatory to protect your health related files also with MFA. This is just to have an idea, you should make this exercise frequently (let's say every 6 months) and verify if the security controls are in place and have to be updated.

For my own devices, I am using this approach:

* Infrastructure: I am using a password manager with MFA for all my accounts and where is possible I have enabled MFA. I have Cloudflare ZT on my home network, so I am a bit protected against web threat. Moreover, I have a script that everyday download phishing and malicious feeds and update my router's ACLs. I am not exposing anything on public, all the services inside my house are accessible through VPN. My Chinese camera are heavy firewalled in a different VLAN and reachable only from specific host. Every device is upgraded to last version and no default passwords.

* Main laptop: is running Linux, so I am feeling a bit more safer during the web surfing. Anyway, I have an encrypted backup for important data over cloud, just to be ensure disaster recovery.

* Secondary laptop: is running Windows, I am keeping it regularly updated with scheduled MS Defender scans. My wife is mainly using it, but she is not installing anything without my approval (I am the admin of the laptop).

* Phone: Storage encrypted, access protected by strong PIN and no biometric. Applications are installed only from official stores and using a DNS blacklist. My phone has a native feature to reduce and auditing app permissions on a schedule and I am doing it by myself as well sometimes. In case I have to connect to an unencrypted public network, I am using a Wireguard VPN client.

Just my 2 cents, I hope to did not forget anything and be helpful.

> don't confuse formal verification with security

It sure makes auditing that code conforms to an expected design a lot easier, which is most security bugs. This is a fantastic design choice for a security focused kernel.

I will grant that proving something was implemented as designed does not rule out design flaws so, fair enough.

Windows does all of those, in addition to fine grained access controls. I would go so far as to say that the Chromium sandbox implementation is better than on Android because of the ability to completely de-privilege processes.

You can try to "snoop" on the virus. For example, collecting all the internet packets, see if some ports are opened that is not needed. Collect logs on which apps are eating up the battery. These steps are not perfect by any means, but you can catch some noisy virus with this. If your virus is very stealthy you can only hope your passwords show up in haveibeenpwned.

This is also why using an open source OS is so important. At least you can investigate why something is happening in the OS. Without the source you can only guess at what is happening.