{"id":890,"date":"2011-11-03T00:32:32","date_gmt":"2011-11-02T23:32:32","guid":{"rendered":"http:\/\/cerezo.name\/blog\/?p=890"},"modified":"2024-10-14T14:10:37","modified_gmt":"2024-10-14T12:10:37","slug":"trust-hypervisors-but-formally-verify-them","status":"publish","type":"post","link":"http:\/\/cerezo.name\/blog\/2011\/11\/03\/trust-hypervisors-but-formally-verify-them\/","title":{"rendered":"Trust (hypervisors), but (formally) verify them"},"content":{"rendered":"<p style=\"text-align: right;\"><span style=\"font-size: large;\"><em>Quis custodiet ipsos custodes?<\/em><\/span><\/p>\n<p style=\"text-align: right;\"><a href=\"http:\/\/www.thelatinlibrary.com\/juvenal\/6.shtml\" target=\"_blank\" rel=\"noopener\">Juvenal, (Satire <span class=\"caps\">VI<\/span>, lines 347\u20138)<\/a><\/p>\n<iframe src=\"https:\/\/www.slideshare.net\/slideshow\/embed_code\/5381924\" width=\"625\" height=\"507\" frameborder=\"0\" marginwidth=\"0\" marginheight=\"0\" scrolling=\"no\"><\/iframe><br>\n<p style=\"text-align: justify;\">It\u2019s been a while since I lectured about the formal construction of Java compilers and virtual machines. But nowadays, all the action has moved to an even more basic layer of the software infrastructure: the <a href=\"http:\/\/en.wikipedia.org\/wiki\/Hypervisor\" target=\"_blank\" rel=\"noopener\">hypervisor<\/a>, the core of the operating system virtual machine manager. But it\u2019s just d\u00e9j\u00e0-vu all over again, an instance of the eternal recurrence in the software world, since the first virtual machines originated at the operating system-level (<a href=\"http:\/\/en.wikipedia.org\/wiki\/IBM_System\/360_Model_67\" target=\"_blank\" rel=\"noopener\"><span class=\"caps\">IBM<\/span> 360 Model 67<\/a>). Even so, verification is still a key step to solve many Gordian knots, rooted in the same fashion of <a href=\"http:\/\/cm.bell-labs.com\/who\/ken\/trust.html\" target=\"_blank\" rel=\"noopener\">Thompson\u2019s Reflections on Trusting Trust<\/a> : from <a href=\"http:\/\/research.microsoft.com\/en-us\/projects\/vcc\/\" target=\"_blank\" rel=\"noopener\">concurrency verification in Hyper\u2011V<\/a> to the more advanced <a href=\"http:\/\/www.cs.cornell.edu\/talc\/\" target=\"_blank\" rel=\"noopener\">Typed Assembly Language<\/a> and <a href=\"http:\/\/www.eecs.berkeley.edu\/~necula\/pcc.html\" target=\"_blank\" rel=\"noopener\" class=\"broken_link\">Proof-Carrying Code<\/a> techniques.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Quis custodiet ipsos custodes? Juvenal, (Satire <span class=\"caps\">VI<\/span>, lines 347\u20138) It\u2019s been a while since I lectured about the formal construction of Java compilers and virtual machines. But nowadays, all the action has moved to an even more basic layer of the software infrastructure: the hypervisor, the core of the operating system virtual machine manager. But&nbsp;[\u2026]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"wp_typography_post_enhancements_disabled":false,"ngg_post_thumbnail":0},"categories":[6],"tags":[],"_links":{"self":[{"href":"http:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/posts\/890"}],"collection":[{"href":"http:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/comments?post=890"}],"version-history":[{"count":6,"href":"http:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/posts\/890\/revisions"}],"predecessor-version":[{"id":1623,"href":"http:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/posts\/890\/revisions\/1623"}],"wp:attachment":[{"href":"http:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/media?parent=890"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/categories?post=890"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/tags?post=890"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}