DeepSpec · JasonGross · Feb 20, 2026 · Feb 20, 2026
diff --git a/coq-sf-secf.opam b/coq-sf-secf.opam
@@ -0,0 +1,37 @@
+opam-version: "2.0"
+homepage: "https://softwarefoundations.cis.upenn.edu/"
+doc: "https://softwarefoundations.cis.upenn.edu/"
+authors: [
+  "Cătălin Hriţcu"
+  "Yonghyun Kim"
+  "Santiago Arranz Olmos"
+  "Gilles Barthe"
+  "Roberto Blanco"
+  "Lionel Blatter"
+  "Léon Ducruet"
+  "Sebastian Harwig"
+  "Benjamin C. Pierce"
+  "Jérémy Thibault"
+]
+license: "like MIT"
+
+build: [
+  [make "-C" "secf-current" "-j%{jobs}%"]
+]
+
+install: [
+  [make "-C" "secf-current" "install"]
+]
+
+bug-reports: "?"
+depends: [
+  "ocaml"
+  "coq"
+]
+synopsis:
+  "Security Foundations (Volume 7 of Software Foundations)"
+description:
+  "Security Foundations covers information-flow security, noninterference, static information-flow control, and constant-time programming."
+url {
+  src: "https://www.cis.upenn.edu/~bcpierce/sf/secf-current/secf.tgz"
+}
diff --git a/secf-current/.devcontainer/.zshrc b/secf-current/.devcontainer/.zshrc
@@ -0,0 +1,13 @@
+autoload -U colors && colors
+precmd() {
+   drawline=""
+   for i in {1..$COLUMNS}; drawline=" $drawline"
+   drawline="%U${drawline}%u"
+   PS1="%F{252}${drawline}
+%B%F{124}%n:%~>%b%f "
+}
+
+eval $(opam env)
+
+alias ls="ls --color"
+
diff --git a/secf-current/.devcontainer/Dockerfile b/secf-current/.devcontainer/Dockerfile
@@ -0,0 +1,58 @@
+FROM ubuntu:20.04
+
+## BEGIN: RUNS AS ROOT
+
+# Create a user
+
+ARG USERNAME=cis5000
+ARG USER_UID=1000
+ARG USER_GID=$USER_UID
+
+RUN apt-get update -y
+
+RUN groupadd --gid $USER_GID $USERNAME \
+    && useradd --uid $USER_UID --gid $USER_GID -m $USERNAME --shell /bin/zsh \
+    #
+    # [Optional] Add sudo support. Omit if you don't need to install software after connecting.
+    && apt-get install -y sudo \
+    && echo $USERNAME ALL=\(root\) NOPASSWD:ALL > /etc/sudoers.d/$USERNAME \
+    && chmod 0440 /etc/sudoers.d/$USERNAME
+
+## Hack needs root permissions
+
+# See hack.sh
+COPY hack.sh /tmp/hack.sh
+RUN chmod +x /tmp/hack.sh
+RUN /tmp/hack.sh
+
+RUN apt-get install -y build-essential
+RUN apt-get install -y linux-libc-dev
+RUN apt-get install -y m4
+RUN apt-get install -y opam
+RUN apt-get install -y time
+RUN apt-get install -y zip
+RUN apt-get install -y zsh
+RUN apt-get install -y libgmp3-dev
+RUN DEBIAN_FRONTEND=noninteractive apt-get install -y pkg-config
+
+## Set up user environmnent
+COPY .zshrc /home/$USERNAME/
+
+
+## Run in usermode
+
+# [Optional] Set the default user. Omit if you want to keep the default as root.
+USER $USERNAME
+
+# Configure opam/ocaml
+RUN opam init -y --disable-sandboxing --compiler=5.3.0
+RUN opam switch 5.3.0
+RUN opam install -y num
+RUN opam repo add -y coq-released https://coq.inria.fr/opam/released
+RUN opam pin add -y coq 9.0.0
+RUN opam install -y coq-simple-io
+RUN opam install -y vscoq-language-server
+RUN opam update -y
+RUN opam upgrade -y
+RUN eval `opam config env`
+
diff --git a/secf-current/.devcontainer/devcontainer.json b/secf-current/.devcontainer/devcontainer.json
@@ -0,0 +1,49 @@
+// For format details, see https://aka.ms/devcontainer.json. For config options, see the
+// README at: https://github.com/devcontainers/templates/tree/main/src/ubuntu
+{
+    "name": "Ubuntu",
+    // Or use a Dockerfile or Docker Compose file. More info: https://containers.dev/guide/dockerfile
+    "build": { 
+	"dockerfile": "Dockerfile"
+    },
+
+    // Features to add to the dev container. More info: https://containers.dev/features.
+    // "features": {},
+
+    // Use 'forwardPorts' to make a list of ports inside the container available locally.
+    // "forwardPorts": [],
+
+    // Use 'postCreateCommand' to run commands after the container is created.
+    // "postCreateCommand": "uname -a",
+
+    // Configure tool-specific properties.
+    "customizations": {
+	"vscode": {
+	    "extensions": [
+		"maximedenes.vscoq"
+	    ],
+	    "settings": {
+		"coqtop.binPath" : "/home/cis5000/.opam/4.14.0/bin",
+		"files.exclude": {
+		    "**/*.aux": true,
+		    "**/*.glob": true,
+		    "**/*.vo": true,
+		    "**/*.vos": true,
+		    "**/*.vok": true,
+		    "**/*.html": true,
+		    "**/.*.report": true,
+		    "**/.*.cache": true
+		},
+		"coq.loadCoqProject": true,
+		"coq.coqProjectRoot": ".",
+		"[coq]": {
+		    "editor.tabSize": 2,
+		    "editor.insertSpaces": true
+		}
+	    }	    
+	}
+    }
+
+    // Uncomment to connect as root instead. More info: https://aka.ms/dev-containers-non-root.
+    // "remoteUser": "root"
+}
diff --git a/secf-current/.devcontainer/hack.sh b/secf-current/.devcontainer/hack.sh
@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+
+### HACK - workaround ubuntu libc6 version number bug see: https://forum.odroid.com/viewtopic.php?p=344373
+
+mv /bin/uname /bin/uname.orig
+tee -a /bin/uname <<EOF
+#!/bin/bash
+if [[ \$1 == "-r" ]]; then
+echo '4.9.250';
+exit
+else
+uname.orig \$1
+fi
+EOF
+
+chmod 755 /bin/uname
+### END HACK
diff --git a/secf-current/Bib.html b/secf-current/Bib.html
@@ -0,0 +1,180 @@
+<!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>Bib: Bibliography</title>
+<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>
+<script src="common/toggleproofs.js"></script>
+<link href="common/css/secf.css" rel="stylesheet" type="text/css"/>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
+<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
+<div class='booktitleinheader'><a href='index.html'>Volume 7: Security Foundations</a></div>
+<ul id='menu'>
+   <li class='section_name'><a href='toc.html'>Table of Contents</a></li>
+   <li class='section_name'><a href='coqindex.html'>Index</a></li>
+   <li class='section_name'><a href='deps.html'>Roadmap</a></li>
+</ul>
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Bib<span class="subtitle">Bibliography</span></h1>
+
+
+<div class="doc">
+
+<div class="paragraph"> </div>
+
+<a id="lab118"></a><h1 class="section">Resources cited in this volume</h1>
+
+<div class="paragraph"> </div>
+
+
+<div class="paragraph"> </div>
+
+<a target="Algehed-and Bernardy 2019"><span class="inlineref"><b>[Algehed and Bernardy 2019]</b></span></a> Simple noninterference from
+  parametricity. Maximilian Algehed, Jean-Philippe Bernardy. Proc. ACM
+  Program. Lang. 3(ICFP): 89:1-89:22. 2019. <a href="https://doi.org/10.1145/3341693"><span class="inlineref" <a href='https://doi.org/10.1145/3341693</span></a>'>https://doi.org/10.1145/3341693</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Algehed-et al 2021"><span class="inlineref"><b>[Algehed et al 2021]</b></span></a> Dynamic IFC Theorems for Free! Maximilian Algehed,
+  Jean-Philippe Bernardy, Catalin Hritcu. CSF 2021. 1-14.
+  <a href="https://arxiv.org/abs/2005.04722"><span class="inlineref" <a href='https://arxiv.org/abs/2005.04722</span></a>'>https://arxiv.org/abs/2005.04722</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Almeida-et al 2020"><span class="inlineref"><b>[Almeida et al 2020]</b></span></a> The Last Mile: High-Assurance and High-Speed
+  Cryptographic Implementations. José Bacelar Almeida, Manuel Barbosa, Gilles
+  Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira,
+  Pierre-Yves Strub. IEEE Symposium on Security and Privacy. 2020.
+  <a href="https://doi.org/10.1109/SP40000.2020.00028"><span class="inlineref" <a href='https://doi.org/10.1109/SP40000.2020.00028</span></a>'>https://doi.org/10.1109/SP40000.2020.00028</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Arranz-Olmos-et al 2025"><span class="inlineref"><b>[Arranz-Olmos et al 2025]</b></span></a> Preservation of Speculative Constant-Time by
+  Compilation. Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin
+  Grégoire, Vincent Laporte. Proc. ACM Program. Lang. 9(POPL):
+  1293-1325. 2025. <a href="https://doi.org/10.1145/3704880"><span class="inlineref" <a href='https://doi.org/10.1145/3704880</span></a>'>https://doi.org/10.1145/3704880</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Barthe-et al 2019"><span class="inlineref"><b>[Barthe et al 2019]</b></span></a> System-Level Non-interference of Constant-Time
+  Cryptography. Part I: Model. Gilles Barthe, Gustavo Betarte, Juan Diego Campo,
+  Carlos Luna. J. Autom. Reason. 63(1): 1-51. 2019.
+  <a href="https://doi.org/10.1007/s10817-017-9441-5"><span class="inlineref" <a href='https://doi.org/10.1007/s10817-017-9441-5</span></a>'>https://doi.org/10.1007/s10817-017-9441-5</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Barthe-et al 2020"><span class="inlineref"><b>[Barthe et al 2020]</b></span></a> Formal verification of a constant-time preserving C
+  compiler. Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin,
+  Vincent Laporte, David Pichardie, Alix Trieu. Proc. ACM
+  Program. Lang. 4(POPL): 7:1-7:30. 2020. <a href="https://doi.org/10.1145/3371075"><span class="inlineref" <a href='https://doi.org/10.1145/3371075</span></a>'>https://doi.org/10.1145/3371075</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Barthe-et al 2021"><span class="inlineref"><b>[Barthe et al 2021]</b></span></a> Structured Leakage and Applications to Cryptographic
+  Constant-Time and Cost. Gilles Barthe, Benjamin Grégoire, Vincent Laporte,
+  Swarn Priya. ACM SIGSAC Conference on Computer and Communications Security
+  (CCS). 2021. <a href="https://doi.org/10.1145/3460120.3484761"><span class="inlineref" <a href='https://doi.org/10.1145/3460120.3484761</span></a>'>https://doi.org/10.1145/3460120.3484761</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Baumann-et al 2025"><span class="inlineref"><b>[Baumann et al 2025]</b></span></a> FSLH: Flexible Mechanized Speculative Load
+  Hardening. Jonathan Baumann, Roberto Blanco, Léon Ducruet, Sebastian Harwig,
+  and Cătălin Hrițcu. IEEE Computer Security Foundations Symposium
+  (CSF). 2025. <a href="http://arxiv.org/abs/2502.03203"><span class="inlineref" <a href='http://arxiv.org/abs/2502.03203</span></a>'>http://arxiv.org/abs/2502.03203</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Devriese-and Piessens 2010"><span class="inlineref"><b>[Devriese and Piessens 2010]</b></span></a> Noninterference through Secure
+  Multi-execution. Dominique Devriese, Frank Piessens. IEEE Symposium on
+  Security and Privacy. 2010.  <a href="https://doi.org/10.1109/SP.2010.15"><span class="inlineref" <a href='https://doi.org/10.1109/SP.2010.15</span></a>'>https://doi.org/10.1109/SP.2010.15</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Lau-et al 2024"><span class="inlineref"><b>[Lau et al 2024]</b></span></a> Specification and Verification of Strong Timing Isolation
+  of Hardware Enclaves. Stella Lau, Thomas Bourgeat, Clément Pit-Claudel, Adam
+  Chlipala. ACM SIGSAC Conference on Computer and Communications Security
+  (CCS). 2024. <a href="https://doi.org/10.1145/3658644.3690203"><span class="inlineref" <a href='https://doi.org/10.1145/3658644.3690203</span></a>'>https://doi.org/10.1145/3658644.3690203</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Molnar-et al 2005"><span class="inlineref"><b>[Molnar et al 2005]</b></span></a> The Program Counter Security Model: Automatic Detection
+  and Removal of Control-Flow Side Channel Attacks. David Molnar, Matt
+  Piotrowski, David Schultz, and David Wagner. ICISC 2005.
+  <a href="https://eprint.iacr.org/2005/368"><span class="inlineref" <a href='https://eprint.iacr.org/2005/368</span></a>'>https://eprint.iacr.org/2005/368</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Ngo-et al 2018"><span class="inlineref"><b>[Ngo et al 2018]</b></span></a> Impossibility of Precise and Sound Termination-Sensitive
+  Security Enforcements. Minh Ngo, Frank Piessens, Tamara Rezk. IEEE Symposium
+  on Security and Privacy. 2018. <a href="https://doi.org/10.1109/SP.2018.00048"><span class="inlineref" <a href='https://doi.org/10.1109/SP.2018.00048</span></a>'>https://doi.org/10.1109/SP.2018.00048</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Sabelfeld-and Myers 2003"><span class="inlineref"><b>[Sabelfeld and Myers 2003]</b></span></a> Language-based information-flow security.  Andrei
+  Sabelfeld and Andrew C. Myers. IEEE Journal on Selected Areas in
+  Communications 21 (1), 5-19. 2003.
+  <a href="https://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf"><span class="inlineref" <a href='https://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf</span></a>'>https://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Shivakumar-et al 2023"><span class="inlineref"><b>[Shivakumar et al 2023]</b></span></a> Spectre Declassified: Reading from the Right Place
+  at the Wrong Time. B. A. Shivakumar, J. Barnes, G. Barthe, S. Cauligi,
+  C. Chuengsatiansup, D. Genkin, S. O’Connell, P. Schwabe, R. Q. Sim, and
+  Y. Yarom.  IEEE Symposium on Security and Privacy. 2023.
+  <a href="http://dx.doi.org/10.1109/SP46215.2023.10179355"><span class="inlineref" <a href='http://dx.doi.org/10.1109/SP46215.2023.10179355</span></a>'>http://dx.doi.org/10.1109/SP46215.2023.10179355</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Volpano-et al 1996"><span class="inlineref"><b>[Volpano et al 1996]</b></span></a> A Sound Type System for Secure Flow Analysis. Dennis
+  M. Volpano, Cynthia E. Irvine, Geoffrey Smith. J. Comput. Secur. 4(2/3):
+  167-188. 1996. <a href="https://people.mpi-sws.org/~dg/teaching/lis2014/modules/ifc-1-volpano96.pdf"><span class="inlineref" <a href='https://people.mpi-sws.org/~dg/teaching/lis2014/modules/ifc-1-volpano96.pdf</span></a>'>https://people.mpi-sws.org/~dg/teaching/lis2014/modules/ifc-1-volpano96.pdf</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Volpano-and Smith 1997"><span class="inlineref"><b>[Volpano and Smith 1997]</b></span></a> Eliminating Covert Flows with Minimum
+  Typings. Dennis M. Volpano, Geoffrey Smith. Computer Security Foundations
+  Workshop
+  (CSFW). 1997. <a href="https://ifc-challenge.appspot.com/static/pdfs/csfw97.pdf"><span class="inlineref" <a href='https://ifc-challenge.appspot.com/static/pdfs/csfw97.pdf</span></a>'>https://ifc-challenge.appspot.com/static/pdfs/csfw97.pdf</span></a></a>
+
+<div class="paragraph"> </div>
+
+<a target="Zhang-et al 2023"><span class="inlineref"><b>[Zhang et al 2023]</b></span></a> Ultimate SLH: Taking Speculative Load Hardening to the
+  Next Level. Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter
+  Schwabe, Yuval Yarom. USENIX Security Symposium. 2023.
+  <a href="https://www.usenix.org/conference/usenixsecurity23/presentation/zhang-zhiyuan-slh"><span class="inlineref" <a href='https://www.usenix.org/conference/usenixsecurity23/presentation/zhang-zhiyuan-slh</span></a>'>https://www.usenix.org/conference/usenixsecurity23/presentation/zhang-zhiyuan-slh</span></a></a>
+
+<div class="paragraph"> </div>
+
+
+<div class="paragraph"> </div>
+
+
+</div>
+<div class="code">
+
+<span class="comment">(*&nbsp;2026-01-07&nbsp;13:37&nbsp;*)</span><br/>
+</div>
+</div>
+
+<div id="footer">
+<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://rocq-prover.org/">coqdoc</a>
+</div>
+
+</div>
+
+</body>
+</html>