This is the same security fallacy as I mentioned twice before, just reworded. Removing code does not leave you with secure code. There's still a memory allocator, I/O layer, a tcp/ip stack, DHCP protocol+service, HTTP protocol+service, HTTPS protocol+service (edit: sorry, there's no HTTPS support in Mirage), and all of the miscellaneous parts required to run those bits, which all have security concerns.
These are the exact same things you expose to vulnerability in a regular Unix OS, and have the exact same potential flaws. Code doesn't become more secure just because you have to use an ABI. Computers (and security) are not magic.
And provable security, really? First of all, proofs have bugs. Second, no real-world attackers have ever been stopped by a provably secure design (partly because implementation is never provably secure). And finally, Mirage was only written to be a statically-typed low-overhead binary that encourages more code reuse. It was not designed with security in mind. That shows that it's nowhere near provable security to begin with, and real-world attackers won't care either way.
Until you present some proof of any vulnerability, your word has not more weight than mine, and I claim that you don't understand what you talk about and that you can't find a way to compromise her setup.
These are the exact same things you expose to vulnerability in a regular Unix OS, and have the exact same potential flaws. Code doesn't become more secure just because you have to use an ABI. Computers (and security) are not magic.
And provable security, really? First of all, proofs have bugs. Second, no real-world attackers have ever been stopped by a provably secure design (partly because implementation is never provably secure). And finally, Mirage was only written to be a statically-typed low-overhead binary that encourages more code reuse. It was not designed with security in mind. That shows that it's nowhere near provable security to begin with, and real-world attackers won't care either way.