Mobile phone security gets a boost from a formally proven hypervisor program. We all know about the security challenges of personal computers: they get hacked, viruses hijack machines, and keystroke loggers steal passwords that then end up on public Web sites. Yet the amount of security-critical transactions conducted on such systems is steadily increasing. Now think about smart phones and so-called mobile Internet devices, which are increasingly being used for critical transactions and which may replace PCs as the access device of choice for most Web services. These devices are, in many respects, starting to resemble PCs albeit with a much more convenient form factor. Does this mean that they will be as prone to security exploits, and that we are heading towards full-scale disaster as far as the security of our Web services is concerned? We might be, if we don't do something about it. The good news is that the technology to protect us exists.