{"id":6588,"date":"2021-12-01T12:53:49","date_gmt":"2021-12-01T12:53:49","guid":{"rendered":"https:\/\/www.digitalfutures.kth.se\/?page_id=6588"},"modified":"2022-03-17T15:25:13","modified_gmt":"2022-03-17T15:25:13","slug":"roberto-guanciale","status":"publish","type":"page","link":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/research\/digital-futures-fellows\/roberto-guanciale\/","title":{"rendered":"Roberto Guanciale"},"content":{"rendered":"<div class=\"paragraphs\">\n<p><i>Title of the project<br \/>\n<\/i><strong>Toward secure critical systems via verification<\/strong><\/p>\n<p><em><span class=\"TextRun MacChromeBold SCXW159808564 BCX0\" lang=\"EN-US\" xml:lang=\"EN-US\" data-contrast=\"auto\"><span class=\"NormalTextRun SCXW159808564 BCX0\">Background<\/span><span class=\"NormalTextRun SCXW159808564 BCX0\">\u00a0<\/span><span class=\"NormalTextRun SCXW159808564 BCX0\">and summary of fellowship<\/span><span class=\"NormalTextRun SCXW159808564 BCX0\">:<br \/>\n<\/span><\/span><\/em><span data-contrast=\"auto\">One of the main causes of the insecurity of IT systems is complexity. For example, the Linux kernel has been designed to run on all possible platforms (including our\u00a0IoT\u00a0light bulb, the largest supercomputer, and the International Space Station) and includes all sorts of features to accommodate several usage scenarios. Even if the kernel is a foundational part of the majority of our software infrastructure and has been developed by high-quality engineers, this complexity results in 30\u00a0million\u00a0lines of code that are virtually impossible to implement correctly. The kernel contains thousands of documented bugs and an unknown number of undiscovered issues. This leaves fertile ground for attackers that can steal our data, use our resources to mine bitcoins, or take complete control of our systems.<\/span><span data-ccp-props=\"{}\">\u00a0<\/span><\/p>\n<p><span data-contrast=\"auto\">We believe that systems should be developed with much more rigorous techniques. We develop methods to mathematically model hardware and software systems and techniques to verify with mathematical precision the impossibility of vulnerabilities. Even if these techniques are heavy-duty, we focus our research on the analysis of the components that\u00a0constitute the\u00a0root of trust of the IT infrastructure, with the goal of demonstrating that faults of untrusted applications can be securely contained and that cannot affect the critical part of the system. That is, we do not aim to guarantee that\u00a0PokenGo\u00a0is bug-free, but we can mathematically rule out that its bugs can be used to steal your\u00a0BankID\u00a0or your crypto wallet. In particular, we are currently focusing on developing the theories to prevent recent famous vulnerabilities (e.g.\u00a0Spectre) that are caused by low-level processor optimizations.<\/span><span data-ccp-props=\"{}\">\u00a0<\/span><\/p>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Toward secure critical systems via verification<\/p>\n","protected":false},"author":46,"featured_media":0,"parent":6563,"menu_order":232,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-6588","page","type-page","status-publish","hentry"],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v27.8 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>Roberto Guanciale &#8212; Digital Futures<\/title>\n<meta name=\"robots\" content=\"noindex, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<meta property=\"og:locale\" content=\"en_GB\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Roberto Guanciale &#8212; Digital Futures\" \/>\n<meta property=\"og:description\" content=\"Toward secure critical systems via verification\" \/>\n<meta property=\"og:url\" content=\"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/research\/digital-futures-fellows\/roberto-guanciale\/\" \/>\n<meta property=\"og:site_name\" content=\"Digital Futures\" \/>\n<meta property=\"article:modified_time\" content=\"2022-03-17T15:25:13+00:00\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Estimated reading time\" \/>\n\t<meta name=\"twitter:data1\" content=\"2 minutes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\\\/\\\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/research\\\/digital-futures-fellows\\\/roberto-guanciale\\\/\",\"url\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/research\\\/digital-futures-fellows\\\/roberto-guanciale\\\/\",\"name\":\"Roberto Guanciale &#8212; Digital Futures\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/#website\"},\"datePublished\":\"2021-12-01T12:53:49+00:00\",\"dateModified\":\"2022-03-17T15:25:13+00:00\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/research\\\/digital-futures-fellows\\\/roberto-guanciale\\\/#breadcrumb\"},\"inLanguage\":\"en-GB\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/research\\\/digital-futures-fellows\\\/roberto-guanciale\\\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/research\\\/digital-futures-fellows\\\/roberto-guanciale\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Research\",\"item\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/research\\\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"Digital Futures Fellows\",\"item\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/research\\\/digital-futures-fellows\\\/\"},{\"@type\":\"ListItem\",\"position\":4,\"name\":\"Roberto Guanciale\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/#website\",\"url\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/\",\"name\":\"Digital Futures\",\"description\":\"\",\"publisher\":{\"@id\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/#organization\"},\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"en-GB\"},{\"@type\":\"Organization\",\"@id\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/#organization\",\"name\":\"Digital Futures\",\"url\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/\",\"logo\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-GB\",\"@id\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/#\\\/schema\\\/logo\\\/image\\\/\",\"url\":\"\\\/wp-content\\\/uploads\\\/sites\\\/7\\\/2020\\\/11\\\/df_black_hires.png\",\"contentUrl\":\"\\\/wp-content\\\/uploads\\\/sites\\\/7\\\/2020\\\/11\\\/df_black_hires.png\",\"width\":5870,\"height\":856,\"caption\":\"Digital Futures\"},\"image\":{\"@id\":\"https:\\\/\\\/wpmu-tris.sys.kth.se\\\/digitalfutures\\\/#\\\/schema\\\/logo\\\/image\\\/\"}}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Roberto Guanciale &#8212; Digital Futures","robots":{"index":"noindex","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"og_locale":"en_GB","og_type":"article","og_title":"Roberto Guanciale &#8212; Digital Futures","og_description":"Toward secure critical systems via verification","og_url":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/research\/digital-futures-fellows\/roberto-guanciale\/","og_site_name":"Digital Futures","article_modified_time":"2022-03-17T15:25:13+00:00","twitter_card":"summary_large_image","twitter_misc":{"Estimated reading time":"2 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/research\/digital-futures-fellows\/roberto-guanciale\/","url":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/research\/digital-futures-fellows\/roberto-guanciale\/","name":"Roberto Guanciale &#8212; Digital Futures","isPartOf":{"@id":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/#website"},"datePublished":"2021-12-01T12:53:49+00:00","dateModified":"2022-03-17T15:25:13+00:00","breadcrumb":{"@id":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/research\/digital-futures-fellows\/roberto-guanciale\/#breadcrumb"},"inLanguage":"en-GB","potentialAction":[{"@type":"ReadAction","target":["https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/research\/digital-futures-fellows\/roberto-guanciale\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/research\/digital-futures-fellows\/roberto-guanciale\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/"},{"@type":"ListItem","position":2,"name":"Research","item":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/research\/"},{"@type":"ListItem","position":3,"name":"Digital Futures Fellows","item":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/research\/digital-futures-fellows\/"},{"@type":"ListItem","position":4,"name":"Roberto Guanciale"}]},{"@type":"WebSite","@id":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/#website","url":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/","name":"Digital Futures","description":"","publisher":{"@id":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/#organization"},"potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"en-GB"},{"@type":"Organization","@id":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/#organization","name":"Digital Futures","url":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/","logo":{"@type":"ImageObject","inLanguage":"en-GB","@id":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/#\/schema\/logo\/image\/","url":"\/wp-content\/uploads\/sites\/7\/2020\/11\/df_black_hires.png","contentUrl":"\/wp-content\/uploads\/sites\/7\/2020\/11\/df_black_hires.png","width":5870,"height":856,"caption":"Digital Futures"},"image":{"@id":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/#\/schema\/logo\/image\/"}}]}},"_links":{"self":[{"href":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/wp-json\/wp\/v2\/pages\/6588","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/wp-json\/wp\/v2\/users\/46"}],"replies":[{"embeddable":true,"href":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/wp-json\/wp\/v2\/comments?post=6588"}],"version-history":[{"count":6,"href":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/wp-json\/wp\/v2\/pages\/6588\/revisions"}],"predecessor-version":[{"id":8087,"href":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/wp-json\/wp\/v2\/pages\/6588\/revisions\/8087"}],"up":[{"embeddable":true,"href":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/wp-json\/wp\/v2\/pages\/6563"}],"wp:attachment":[{"href":"https:\/\/wpmu-tris.sys.kth.se\/digitalfutures\/wp-json\/wp\/v2\/media?parent=6588"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}