-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
65 lines (64 loc) · 9.87 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>SILC: Secure Interoperability, Languages, and Compilers</title>
<link rel="icon" type="image/png" sizes="16x16" href="./static/img/favicon-16x16.png">
<link rel="icon" type="image/png" sizes="32x32" href="./static/img/favicon-32x32.png">
<link rel="icon" type="image/png" sizes="96x96" href="./static/img/favicon-96x96.png">
<link href="https://fonts.googleapis.com/css?family=Montserrat" rel="stylesheet">
<link href="https://code.cdn.mozilla.net/fonts/fira.css" rel=" stylesheet">
<link rel="stylesheet" type="text/css" href="./css/main.css" />
</head>
<body>
<div id="top-wrap">
<div id="top">
<span class="content">
<h1><img src="./static/img/logo.svg" width="240px"></h1>
<h1>Secure Interoperability, Languages, and Compilers</h1>
</span>
</div>
</div>
<div id="middle-wrap">
<div id="top-border"></div>
<ul id="nav">
<li><a class="active" href="./">Home</a></li>
<li><a href="./projects">Projects</a></li>
<li><a href="./publications">Publications</a></li>
<li><a href="./people">People</a></li>
</ul>
<div id="middle">
<p>Despite considerable progress in compiler verification in recent years, verified compilers are still proved correct under unreasonable assumptions about what the compiled code will be linked with. These assumptions range from no linking at all—i.e., that compilation units are whole programs—to linking only with code compiled by the same compiler or from the same source language. Such assumptions contradict the reality of how we use compilers in today’s world of multi-language software where most software systems are comprised of <em>components</em> written in <em>different languages</em> compiled by <em>different compilers</em> to a common target, as well as runtime-library routines handwritten in the target language.</p>
<p>The SILC group is investigating techniques for principled compilation and secure interoperability in a world of multi-language software. Our recent research on compositional compiler correctness (or correct compilation of <em>components</em>) has led us to the conclusion that compositional compiler correctness is fundamentally a multi-language problem: solutions to this problem demand both novel language design, in the form of principled FFIs for languages, as well as compilers that preserve type specifications and correctness of refactoring to ensure safe linking with code compiled from other languages.</p>
<p>Our long-term vision is to have verified compilers from languages as different as C, ML, Rust, and Gallina—the specification language of the Coq proof assistant—to a common low-level, richly (and gradually) typed WebAssembly-like target language that enforces safe interoperability between components compiled from more precisely typed, less precisely typed, and untyped source languages.<br />
In pursuit of this vision, we have made progress on challenging problems in a number of areas relevant to correct and secure compilation in the setting of multi-language software.</p>
<ul>
<li><p>Language interoperability and compiler correctness: We take the point of view that <em>compositional compiler correctness is a language interoperability problem</em> (<a href="http://www.ccs.neu.edu/home/amal/papers/verifcomp.pdf">Ahmed 2015</a>): embedding a single-language fragment in a multi-language system affects the notion of program equivalence that the compiler must use when reasoning about the correctness of optimizations. But the precise notion of equivalence can be adjusted by modifying the rules governing interoperability (linking) in the multi-language system. We have developed a novel specification of<br />
compositional compiler correctness that requires that if a source component <code>s</code> compiles to a target component <code>t</code>, then <code>t</code> linked with some arbitrary target code <code>t'</code> should behave the same as <code>s</code> interoperating with <code>t'</code>. To express the latter, we give a formal semantics of interoperability between (high-level) source components and (low-level) target code. Our group has used <em>source-target multi-language semantics</em> for the verification of several compiler transformations (<a href="http://www.ccs.neu.edu/home/amal/papers/voc.pdf">Perconti and Ahmed 2014</a>, <a href="http://plt.eecs.northwestern.edu/blame-for-all/">Ahmed and Blume 2011</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/fabcc.pdf">New et al. 2016</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/refcc.pdf">Ahmed et al. 2016</a>).</p></li>
<li><p>Gradual typing: We have also done work on <em>gradual typing</em>—which ensures safe interoperability between statically and dynamically typed code—in the presence of polymorphism (<a href="http://www.ccs.neu.edu/home/amal/papers/parpolyseal.pdf">Matthews and Ahmed 2008</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/blame-all.pdf">Ahmed et al 2009</a>, <a href="http://plt.eecs.northwestern.edu/blame-for-all/">Ahmed et al 2011</a>, <a href="http://drops.dagstuhl.de/opus/volltexte/2018/9194/">New and Licata 2018</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/graduality.pdf">New and Ahmed 2018</a>). Most recently, we have advocated that language designers equip their core languages with <em>linking types</em>, a form of safe FFIs, to give programmers the ability to specify how their components should interoperate with features that cannot be expressed in their language.</p></li>
<li><p>Type-preserving and refactoring-preserving compilation: We are investigating type-preserving compilers for a variety of languages to prevent compiled components from being linked with ill-behaved target clients. A type-preserving compiler preserves invariants and specifications from the source program into the target program and can use these types to prevent linking with target code that might violate source-language type safety or invalidate correctness of source-level refactoring. We have done work on type-preserving compilers for ML-like languages, as well as dependently typed languages (<a href="http://www.ccs.neu.edu/home/amal/papers/cpscc.pdf">Bowman et al 2018</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/closconvcc.pdf">Bowman and Ahmed 2018</a>).</p></li>
<li><p>Proof methods for program equivalence: Verifying correct compilation of <em>components</em> requires proof methods for establishing that the behavior of a source component is <em>equivalent</em> to the behavior of the compiled component. <em>Logical relations</em> are a well-known method for proving equivalence of program components, and our work on <em>step-indexed logical relations</em> has shown how to scale the method to realistic (typed and untyped) languages with features such as ML- and Java-style mutable references, recursive types, polymorphism, and concurrency (<a href="http://www.cs.princeton.edu/research/techreps/TR-713-04">Ahmed 2004</a>, <a href="http://portal.acm.org/citation.cfm?doid=1709093.1709094">Ahmed et al 2010</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/lr-recquant.pdf">Ahmed 2006</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/impselfadj.pdf">Acar et al 2008</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/sdri.pdf">Ahmed et al 2009</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/lslr.pdf">Dreyer et al 2009</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/relcon.pdf">Turon et al. 2012</a>). We have also shown how to extend logical relations to support reasoning about equivalence in several mixed-language settings (<a href="http://www.ccs.neu.edu/home/amal/papers/parpolyseal.pdf">Matthews and Ahmed 2008</a>, <a href="http://plt.eecs.northwestern.edu/blame-for-all/">Ahmed et al 2011</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/voc.pdf">Perconti et al. 2014</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/fabcc.pdf">New et al. 2016</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/refcc.pdf">Ahmed et al. 2016</a>, <a href="http://www.ccs.neu.edu/home/amal/papers/funtal.pdf">Patterson et al. 2017</a>).</p></li>
</ul>
<div class="small">
<h2 id="research-funding">Research funding</h2>
<ul>
<li>NSF: Principled Compiling and Linking for Multi-Language Software (<a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=1816837&HistoricalAwards=false">CCF-1816837</a>, 10/2018-9/2021)</li>
<li>NSF Graduate Research Fellowship for Aaron Weiss (<a href="https://nsfgrfp.org">2017-2022</a>)</li>
<li>NSF: Foundations of Just-in-Time Compilation (<a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=1618732&HistoricalAwards=false">CCF-1618732</a>, 9/2016-8/2018)</li>
<li>NSF CAREER: Verified Compilers for a Multi-Language World (<a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=1453796&HistoricalAwards=false">CCF-1453796</a>, 5/2015-4/2020)</li>
<li>NSF: Secure Compilation of Advanced Languages (<a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=1422133&HistoricalAwards=false">CCF-1422133</a>, 8/2014-7/2017)</li>
<li>Google Faculty Research Award: Verified Compilers for a Multi-Language World, (<a href="https://ai.googleblog.com/2014/02/google-research-awards-winter-2014.html">2014</a>)</li>
<li>NSF: Effectful Software Contracts (<a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=1117635&HistoricalAwards=false">CCF-1203008</a>, 8/2011-7/2014)</li>
</ul>
</div>
</div>
</div>
<div id="bottom-wrap">
<div id="bottom-border"></div>
<div id="bottom">
<a href="./">SILC</a> is part of the <a href="http://prl.ccs.neu.edu" target="_blank">Programming Research Laboratory</a> at <a href="http://ccs.neu.edu" target="_blank">Northeastern University</a>.
</div>
</div>
</body>
</html>