Postscript.html

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Postscript</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
<ul id='menu'>
   <a href='index.html'><li class='section_name'>PL Foundations</li></a>
   <a href='toc.html'><li>Table of Contents</li></a>
   <a href='coqindex.html'><li>Index</li></a>
   <a href='deps.html'><li>Roadmap</li></a>
</ul>
</div>

<div id="main">

<h1 class="libtitle">Postscript</h1>


<div class="doc">

<div class="paragraph"> </div>

 Congratulations: We've made it to the end! 
<div class="paragraph"> </div>

<a name="lab584"></a><h1 class="section">Looking Back</h1>

<div class="paragraph"> </div>

 We've covered a lot of ground.  Here's a quick review of the whole course starting with <i>Logical Foundations</i>...  

<div class="paragraph"> </div>

<ul class="doclist">
<li> <i>Functional programming</i>:
<ul class="doclist">
<li> "declarative" programming style (recursion over persistent
            data structures, rather than looping over mutable arrays
            or pointer structures)

</li>
<li> higher-order functions

</li>
<li> polymorphism 
</li>
</ul>

</li>
</ul>

<div class="paragraph"> </div>


<div class="paragraph"> </div>

<ul class="doclist">
<li> <i>Logic</i>, the mathematical basis for software engineering:
<pre>
               logic                        calculus
        --------------------   ~   ----------------------------
        software engineering       mechanical/civil engineering
</pre>

<div class="paragraph"> </div>

<ul class="doclist">
<li> inductively defined sets and relations

</li>
<li> inductive proofs

</li>
<li> proof objects 
</li>
</ul>

</li>
</ul>

<div class="paragraph"> </div>


<div class="paragraph"> </div>

<ul class="doclist">
<li> <i>Coq</i>, an industrial-strength proof assistant
<ul class="doclist">
<li> functional core language

</li>
<li> core tactics

</li>
<li> automation

</li>
</ul>

</li>
</ul>

<div class="paragraph"> </div>


<div class="paragraph"> </div>

<ul class="doclist">
<li> <i>Foundations of programming languages</i>

<ul class="doclist">
<li> notations and definitional techniques for precisely specifying
<ul class="doclist">
<li> abstract syntax

</li>
<li> operational semantics
<ul class="doclist">
<li> big-step style

</li>
<li> small-step style

</li>
</ul>

</li>
<li> type systems

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> program equivalence

<div class="paragraph"> </div>


</li>
<li> Hoare logic

<div class="paragraph"> </div>


</li>
<li> fundamental metatheory of type systems

<div class="paragraph"> </div>

<ul class="doclist">
<li> progress and preservation

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> theory of subtyping

</li>
</ul>

</li>
</ul>

</div>

<div class="doc">
<a name="lab585"></a><h1 class="section">Looking Around</h1>

<div class="paragraph"> </div>

 Large-scale applications of these core topics can be found
    everywhere, both in ongoing research projects and in real-world
    software systems.  Here are a few recent examples involving
    formal, machine-checked verification of real-world software and
    hardware systems, to give a sense of what is being done
    today... 
<div class="paragraph"> </div>

<a name="lab586"></a><h3 class="section">CompCert</h3>
 <i>CompCert</i> is a fully verified optimizing compiler for almost all
    of the ISO C<sub>90</sub> / ANSI C language, generating code for x<sub>86</sub>, ARM,
    and PowerPC processors.  The whole of CompCert is is written in
    Gallina and extracted to an efficient OCaml program using Coq's
    extraction facilities.

<div class="paragraph"> </div>

    "The CompCert project investigates the formal verification of
    realistic compilers usable for critical embedded software. Such
    verified compilers come with a mathematical, machine-checked proof
    that the generated executable code behaves exactly as prescribed
    by the semantics of the source program. By ruling out the
    possibility of compiler-introduced bugs, verified compilers
    strengthen the guarantees that can be obtained by applying formal
    methods to source programs."

<div class="paragraph"> </div>

    In 2011, CompCert was included in a landmark study on fuzz-testing
    a large number of real-world C compilers using the CSmith tool.
    The CSmith authors wrote:

<div class="paragraph"> </div>

<ul class="doclist">
<li> The striking thing about our CompCert results is that the
        middle-end bugs we found in all other compilers are absent. As
        of early 2011, the under-development version of CompCert is
        the only compiler we have tested for which Csmith cannot find
        wrong-code errors. This is not for lack of trying: we have
        devoted about six CPU-years to the task. The apparent
        unbreakability of CompCert supports a strong argument that
        developing compiler optimizations within a proof framework,
        where safety checks are explicit and machine-checked, has
        tangible benefits for compiler users.

</li>
</ul>

<div class="paragraph"> </div>

    <a href="http://compcert.inria.fr"><span class="inlineref">http://compcert.inria.fr</span></a> 
<div class="paragraph"> </div>

<a name="lab587"></a><h3 class="section">seL4</h3>
 <i>seL4</i> is a fully verified microkernel, considered to be the
    world's first OS kernel with an end-to-end proof of implementation
    correctness and security enforcement.  It is implemented in C and
    ARM assembly and specified and verified using Isabelle.  The code
    is available as open source.

<div class="paragraph"> </div>

    "seL4 has been comprehensively formally verified: a rigorous
    process to prove mathematically that its executable code, as it
    runs on hardware, correctly implements the behaviour allowed by
    the specification, and no others. Furthermore, we have proved that
    the specification has the desired safety and security
    properties (integrity and confidentiality)... The verification was
    achieved at a cost that is significantly less than that of
    traditional high-assurance development approaches, while giving
    guarantees traditional approaches cannot provide."

<div class="paragraph"> </div>

    <a href="https://sel4.systems"><span class="inlineref">https://sel4.systems</span></a>. 
<div class="paragraph"> </div>

<a name="lab588"></a><h3 class="section">CertiKOS</h3>
 <i>CertiKOS</i> is a clean-slate, fully verified hypervisor, written in
    CompCert C and verified in Coq.

<div class="paragraph"> </div>

    "The CertiKOS project aims to develop a novel and practical
    programming infrastructure for constructing large-scale certified
    system software. By combining recent advances in programming
    languages, operating systems, and formal methods, we hope to
    attack the following research questions: (1) what OS kernel
    structure can offer the best support for extensibility, security,
    and resilience? (2) which semantic models and program logics can
    best capture these abstractions? (3) what are the right
    programming languages and environments for developing such
    certified kernels? and (4) how to build automation facilities to
    make certified software development really scale?"

<div class="paragraph"> </div>

    <a href="http://flint.cs.yale.edu/certikos/"><span class="inlineref">http://flint.cs.yale.edu/certikos/</span></a> 
<div class="paragraph"> </div>

<a name="lab589"></a><h3 class="section">Ironclad</h3>
 <i>Ironclad Apps</i> is a collection of fully verified web
    applications, including a "notary" for securely signing
    statements, a password hasher, a multi-user trusted counter, and a
    differentially-private database.

<div class="paragraph"> </div>

    The system is coded in the verification-oriented programming
    language Dafny and verified using Boogie, a verification tool
    based on Hoare logic.

<div class="paragraph"> </div>

    "An Ironclad App lets a user securely transmit her data to a
    remote machine with the guarantee that every instruction executed
    on that machine adheres to a formal abstract specification of the
    app’s behavior. This does more than eliminate implementation
    vulnerabilities such as buffer overflows, parsing errors, or data
    leaks; it tells the user exactly how the app will behave at all
    times. We provide these guarantees via complete, low-level
    software verification. We then use cryptography and secure
    hardware to enable secure channels from the verified software to
    remote users."

<div class="paragraph"> </div>

    <a href="https://github.com/Microsoft/Ironclad/tree/master/ironclad-apps"><span class="inlineref">https://github.com/Microsoft/Ironclad/tree/master/ironclad-apps</span></a> 
<div class="paragraph"> </div>

<a name="lab590"></a><h3 class="section">Verdi</h3>
 <i>Verdi</i> is a framework for implementing and formally verifying
    distributed systems.

<div class="paragraph"> </div>

    "Verdi supports several different fault models ranging from
    idealistic to realistic. Verdi's verified system
    transformers (VSTs) encapsulate common fault tolerance
    techniques. Developers can verify an application in an idealized
    fault model, and then apply a VST to obtain an application that is
    guaranteed to have analogous properties in a more adversarial
    environment.  Verdi is developed using the Coq proof assistant,
    and systems are extracted to OCaml for execution. Verdi systems,
    including a fault-tolerant key-value store, achieve comparable
    performance to unverified counterparts."

<div class="paragraph"> </div>

    <a href="http://verdi.uwplse.org"><span class="inlineref">http://verdi.uwplse.org</span></a> 
<div class="paragraph"> </div>

<a name="lab591"></a><h3 class="section">DeepSpec</h3>
 <i>The Science of Deep Specification</i> is an NSF "Expedition"
    project (running from 2016 to 2020) that focuses on the
    specification and verification of full functional correctness of
    both software and hardware.  It also sponsors workshops and summer
    schools.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Website: <a href="http://deepspec.org/"><span class="inlineref">http://deepspec.org/</span></a>

</li>
<li> Overview presentations: 
<ul class="doclist">
<li> <a href="http://deepspec.org/about/"><span class="inlineref">http://deepspec.org/about/</span></a>

</li>
<li> <a href="https://www.youtube.com/watch?v=IPNdsnRWBkk"><span class="inlineref">https://www.youtube.com/watch?v=IPNdsnRWBkk</span></a> 
</li>
</ul>

</li>
</ul>

<div class="paragraph"> </div>

<a name="lab592"></a><h3 class="section">REMS</h3>
 <i>REMS</i> is a european project on Rigorous Engineering of Mainstream
    Systems.  It has produced detailed formal specifications of a wide
    range of critical real-world interfaces, protocols, and APIs,
    including 
      the C language, 
      the ELF linker format,
      the ARM, Power, MIPS, CHERI, and RISC-V instruction sets,
      the weak memory models of ARM and Power processors, and
      POSIX filesystems.

<div class="paragraph"> </div>

    "The project is focussed on lightweight rigorous methods: precise
    specification (post hoc and during design) and testing against
    specifications, with full verification only in some cases. The
    project emphasises building useful (and reusable) semantics and
    tools. We are building accurate full-scale mathematical models of
    some of the key computational abstractions (processor
    architectures, programming languages, concurrent OS interfaces,
    and network protocols), studying how this can be done, and
    investigating how such models can be used for new verification
    research and in new systems and programming language
    research. Supporting all this, we are also working on new
    specification tools and their foundations."

<div class="paragraph"> </div>

    <a href="http://www.cl.cam.ac.uk/~pes20/rems/"><span class="inlineref">http://www.cl.cam.ac.uk/~pes20/rems/</span></a> 
<div class="paragraph"> </div>

<a name="lab593"></a><h3 class="section">Others</h3>

<div class="paragraph"> </div>

 There's much more.  Other projects worth checking out include:

<div class="paragraph"> </div>

<ul class="doclist">
<li> Vellvm (formal specification and verification of LLVM
        optimization passes)

</li>
<li> Zach Tatlock's formally certified browser

</li>
<li> Tobias Nipkow's formalization of most of Java

</li>
<li> The CakeML verified ML compiler

</li>
<li> Greg Morrisett's formal specification of the x<sub>86</sub> instruction
        set and the RockSalt Software Fault Isolation tool (a better,
        faster, more secure version of Google's Native Client)

</li>
<li> Ur/Web, a programming language for verified web applications
        embedded in Coq

</li>
<li> the Princeton Verified Software Toolchain

</li>
</ul>

</div>

<div class="doc">
<a name="lab594"></a><h1 class="section">Looking Forward</h1>

<div class="paragraph"> </div>

 Some good places to learn more...

<div class="paragraph"> </div>

<ul class="doclist">
<li> This book includes several optional chapters covering topics
         that you may find useful.  Take a look at the <a
         href="toc.html">table of contents</a> and the <a
         href="deps.html">chapter dependency diagram</a> to find
         them.

<div class="paragraph"> </div>


</li>
<li> More on Hoare logic and program verification
<ul class="doclist">
<li> The Formal Semantics of Programming Languages: An
              Introduction, by Glynn Winskel <a href="Bib.html#Winskel 1993"><span class="inlineref">[Winskel 1993]</span></a>.

</li>
<li> Many practical verification tools, e.g. Microsoft's
              Boogie system, Java Extended Static Checking, etc.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> More on the foundations of programming languages:
<ul class="doclist">
<li> Concrete Semantics with Isabelle/HOL, by Tobias Nipkow
              and Gerwin Klein <a href="Bib.html#Nipkow 2014"><span class="inlineref">[Nipkow 2014]</span></a>

</li>
<li> Types and Programming Languages, by Benjamin C. Pierce
              <a href="Bib.html#Pierce 2002"><span class="inlineref">[Pierce 2002]</span></a>.

</li>
<li> Practical Foundations for Programming Languages, by
              Robert Harper <a href="Bib.html#Harper 2016"><span class="inlineref">[Harper 2016]</span></a>.

</li>
<li> Foundations for Programming Languages, by John
              C. Mitchell <a href="Bib.html#Mitchell 1996"><span class="inlineref">[Mitchell 1996]</span></a>.

<div class="paragraph"> </div>


<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> Iron Lambda (http://iron.ouroborus.net/) is a collection
          of ​Coq formalisations for functional languages of
          increasing complexity. It fills part of the gap between
          the end of the​ Software Foundations course and what
          appears in current research papers.  The collection has
          at least Progress and Preservation theorems for a number
          of variants of STLC and the polymorphic
          lambda-calculus (System F). 

<div class="paragraph"> </div>


<div class="paragraph"> </div>


</li>
<li> Finally, here are some of the main conferences on programming
         languages and formal verification:
<ul class="doclist">
<li> Principles of Programming Langauges (POPL)

</li>
<li> Programming Language Design and Implementation (PLDI)

</li>
<li> International Conference on Functional Programming (ICFP)

</li>
<li> Computer Aided Verification (CAV)

</li>
<li> Interactive Theorem Proving (ITP)

</li>
<li> Certified Programs and Proofs (CPP)

</li>
<li> SPLASH/OOPSLA conferences

</li>
<li> Principles in Practice workshop (PiP)

</li>
<li> CoqPL workshop 

</li>
</ul>

</li>
</ul>

</div>
<div class="code code-tight">

<br/>
<span class="comment">(*&nbsp;$Date:&nbsp;2017-05-24&nbsp;13:40:13&nbsp;-0400&nbsp;(Wed,&nbsp;24&nbsp;May&nbsp;2017)&nbsp;$&nbsp;*)</span><br/>
</div>
</div>

<div id="footer">
<hr/><a href="coqindex.html">Index</a></div>

</div>

</body>
</html>