{"id":390980,"date":"2017-06-22T11:29:04","date_gmt":"2017-06-22T18:29:04","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?p=390980"},"modified":"2017-06-23T10:50:25","modified_gmt":"2017-06-23T17:50:25","slug":"getting-compilers-right-secure-software","status":"publish","type":"post","link":"https:\/\/www.microsoft.com\/en-us\/research\/blog\/getting-compilers-right-secure-software\/","title":{"rendered":"Getting compilers right: a reliable foundation for secure software"},"content":{"rendered":"<p><em>By <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nlopes\/\" target=\"_blank\" rel=\"noopener noreferrer\">Nuno Lopes<\/a>, Researcher, Microsoft Research Cambridge<\/em><\/p>\n<p>Think compilers cannot compromise the security of your application? Think twice!<\/p>\n<p>Compiler writers work around the clock to continuously deliver better compilers. They are driven by the ever-increasing importance of:<\/p>\n<ul>\n<li>Increasing performance (everyone wants their code to run faster!);<\/li>\n<li>Reducing code size (so that your app can fit on people\u2019s phones);<\/li>\n<li>Reducing energy consumption (it\u2019s nice to not drain phone batteries and to save power in energy-hungry datacenters).<\/li>\n<\/ul>\n\t<iframe\n\t\tsrc=\"https:\/\/www.youtube.com\/embed\/INYEaRyj7Ew?rel=0\"\n\t\twidth=\"560\"\n\t\theight=\"315\"\n\t\taria-label=\"\"\n\t\tallowfullscreen=\"true\">\n\t<\/iframe>\n\t\n<div style=\"height: 20px;\"><\/div>\n<p>Compilers are big: most major compilers consist of several million lines of code. Their development is not stale either: every year, each compiler sees thousands of changes. Their sheer size and complexity, plus the pressure to continuously improve compilers, results in bugs slipping through. These compiler bugs may in turn introduce security vulnerabilities into your program.<\/p>\n<p>Let\u2019s look at a key optimization that removes bounds checks. These are commonly used by memory-safe languages (such as C#, Rust, Swift, etc.) or manually in languages such as C++ to ensure that programs cannot access a memory region that they shouldn\u2019t (to avoid security vulnerabilities). For example, a memory load could look like the following:<\/p>\n<pre style=\"font-size: 16px;\">while (...) {\r\n   if (!in_bounds(buffer, idx))\r\n      trap();\r\n   x = buffer[idx];\r\n}<\/pre>\n<p>Compilers will try very hard to eliminate the bounds check or hoist it out of the loop. Compilers can only do these transformations when they can prove it is safe to do so (e.g., if the check always succeeds). However, a buggy compiler optimization may decide to replace the in_bounds check with true because it mistakenly proved that it wasn\u2019t possible for it to be false, essentially removing the bounds check. This may happen because of a bug in one of the hundreds of thousands of lines of code used to prove that the check wasn\u2019t necessary.<\/p>\n<p>Attacks based on compiler bugs are not yet commonplace, but are not science fiction either. It is possible to take advantage of compiler bugs to, for example, elevate user privileges, bypass authentication mechanisms, or steal information. The existence of these attacks has been known at least since 1974, when the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/csrc.nist.gov\/publications\/history\/karg74.pdf\" target=\"_blank\" rel=\"noopener noreferrer\">Multics security evaluation report<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> mentioned the possibility of injection of security vulnerabilities by compromised or simply buggy compilers. More recently, <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/www.alchemistowl.org\/pocorgtfo\/pocorgtfo08.pdf#page=7\" target=\"_blank\" rel=\"noopener noreferrer\">researchers<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> managed to compromise a machine running Ubuntu and escalate privileges using a publicly known bug in LLVM.<\/p>\n<p>Ensuring that compilers are correct is therefore critical to both the correctness and security of your software. Compiler bugs are hard to detect, yet a single bug can introduce a security vulnerability in your program, or make it compute the wrong result.<\/p>\n<p>Together with academic and industrial partners, Microsoft researchers are working to ensure that compilers are correct. We are approaching the problem from two angles: automatically verifying that new optimizations are correct, and automatically verifying that the output of compilers is correct.<\/p>\n<p>To verify the correctness of optimizations, we have developed <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/provably-correct-peephole-optimizations-alive\/\" target=\"_blank\" rel=\"noopener noreferrer\">Alive<\/a>. It consists of a DSL to specify peephole optimizations and a tool to automatically prove that an optimization is correct, or else provide a counterexample showing why the optimization is wrong. You can try Alive <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/Alive\" target=\"_blank\" rel=\"noopener noreferrer\">online<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.<\/p>\n<p>Alive verifies that an optimization is correct by checking for each possible input that the code after optimization is a <em>refinement<\/em> of the code before optimization. In practice, Alive uses the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/Z3Prover\/z3\" target=\"_blank\" rel=\"noopener noreferrer\">Z3 SMT solver<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> to automatically prove small theorems about the optimization that imply that it is correct.<\/p>\n<p><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/rise4fun.com\/Alive\/QPg6\" target=\"_blank\" rel=\"noopener noreferrer\"><img loading=\"lazy\" decoding=\"async\" class=\"alignright wp-image-391373\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2017\/06\/Sidebar_codesnip.png\" alt=\"Microsoft compilers\" width=\"500\" height=\"309\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2017\/06\/Sidebar_codesnip.png 652w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2017\/06\/Sidebar_codesnip-300x185.png 300w\" sizes=\"auto, (max-width: 500px) 100vw, 500px\" \/><span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/p>\n<p>Alive is now used by compiler developers on several compiler teams, including our own C++ compiler team, and also at other companies that develop LLVM. Alive has found dozens of bugs in LLVM and prevented many more from being introduced in LLVM and in Microsoft\u2019s C++ compiler.<\/p>\n<p>We also are working on verifying that the output of compilers is correct. Instead of verifying upfront that an optimization is valid for all input programs, we verify at compile time that the optimization behaved correctly for the particular input it was given (i.e., your program). This approach is called translation validation. Translation validation works by taking a snapshot of the intermediate representation (IR) before and after each optimization and automatically proving that the latter is a refinement of the former.<\/p>\n<p>Translation validation is a powerful ally for verification: first we can support older code that may be out of reach for current automated verification techniques, and second, it provides an extra safety net.<\/p>\n<p>Our translation validation project is codenamed utcTV (short for translation validation for UTC \u2013 Microsoft\u2019s C++ compiler). It is still under development, but already has identified several bugs in development versions of the compiler that were not found using other methods. We will share more details about this project in the future.<\/p>\n<p>A related line of work we are pursuing is on semantics of compiler IRs. How can you verify that something is correct if you don\u2019t know what it really means? That\u2019s why we\u2019ve been studying the semantics of modern compiler IRs, and how to fix the inconsistencies we\u2019ve discovered. More details are available in our <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/taming-undefined-behavior-llvm\/\" target=\"_blank\" rel=\"noopener noreferrer\">upcoming paper<\/a> that we&#8217;ll be presenting at <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/pldi17.sigplan.org\/home\" target=\"_blank\" rel=\"noopener noreferrer\">PLDI \u201917 <span class=\"sr-only\"> (opens in new tab)<\/span><\/a>in Barcelona later this month.<\/p>\n<p>Clearly, it is important to make sure your compiler is working correctly, both for protecting the entire stack, and for reducing exploitable security vulnerabilities in applications. The tools we are working on are designed to automatically prove the correctness of parts of compilers. Microsoft will continue working with its partners to ensure there are no bugs in compilers that may compromise your application\u2019s correctness and security.<\/p>\n<p><strong>Related<\/strong><\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/web.ist.utl.pt\/nuno.lopes\/pubs.php?id=undef-pldi17\">Taming Undefined Behavior in LLVM<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/blogs.msdn.microsoft.com\/vcblog\/2016\/05\/04\/new-code-optimizer\/\">Introducing a new, advanced Visual C++ code optimizer<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/github.com\/nunoplopes\/alive\">Alive: Automatic LLVM&#8217;s Instcombine Verifier<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p><em>Editor\u2019s Note: Microsoft is a Silver sponsor of this year\u2019s PLDI Conference taking place in Barcelona, June 18-23. PLDI is the premier forum in the field of programming languages and programming systems research.<\/em><\/p>\n","protected":false},"excerpt":{"rendered":"<p>By Nuno Lopes, Researcher, Microsoft Research Cambridge Think compilers cannot compromise the security of your application? Think twice! Compiler writers work around the clock to continuously deliver better compilers. They are driven by the ever-increasing importance of: Increasing performance (everyone wants their code to run faster!); Reducing code size (so that your app can fit [&hellip;]<\/p>\n","protected":false},"author":39507,"featured_media":391058,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":[],"msr_hide_image_in_river":0,"footnotes":""},"categories":[194488,194489],"tags":[235610,186569,186414,235613],"research-area":[13560,13558],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-390980","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-program-languages-and-software-engineering","category-security","tag-compiler-bugs","tag-compilers","tag-security","tag-security-vulnerabilities","msr-research-area-programming-languages-software-engineering","msr-research-area-security-privacy-cryptography","msr-locale-en_us"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"","podcast_episode":"","msr_research_lab":[],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[],"related-projects":[],"related-events":[],"related-researchers":[],"msr_type":"Post","featured_image_thumbnail":"<img width=\"626\" height=\"280\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2017\/06\/compilers_video-capture-feature3.png\" class=\"img-object-cover\" alt=\"\" decoding=\"async\" loading=\"lazy\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2017\/06\/compilers_video-capture-feature3.png 626w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2017\/06\/compilers_video-capture-feature3-300x134.png 300w\" sizes=\"auto, (max-width: 626px) 100vw, 626px\" \/>","byline":"","formattedDate":"June 22, 2017","formattedExcerpt":"By Nuno Lopes, Researcher, Microsoft Research Cambridge Think compilers cannot compromise the security of your application? Think twice! Compiler writers work around the clock to continuously deliver better compilers. They are driven by the ever-increasing importance of: Increasing performance (everyone wants their code to run&hellip;","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/390980","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/users\/39507"}],"replies":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/comments?post=390980"}],"version-history":[{"count":20,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/390980\/revisions"}],"predecessor-version":[{"id":393251,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/390980\/revisions\/393251"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/391058"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=390980"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/categories?post=390980"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/tags?post=390980"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=390980"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=390980"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=390980"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=390980"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=390980"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=390980"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=390980"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=390980"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}