Using Kani to Validate Security Boundaries in AWS Firecracker (#42)

Signed-off-by: Patrick Roy <[email protected]> Signed-off-by: Felipe R. Monteiro <[email protected]> Co-authored-by: Felipe R. Monteiro <[email protected]> Co-authored-by: jaisnan <[email protected]>
model-checking · Sep 1, 2023 · 83d98f3 · 83d98f3
1 parent 59bc1c5
commit 83d98f3
Show file tree

Hide file tree

Showing 7 changed files with 315 additions and 1 deletion.
diff --git a/Gemfile.lock b/Gemfile.lock
@@ -67,6 +67,7 @@ GEM
     webrick (1.7.0)
 
 PLATFORMS
+  arm64-darwin-22
   x86_64-darwin-19
   x86_64-darwin-21
 

diff --git a/_config.yml b/_config.yml
@@ -8,7 +8,7 @@
 # For technical reasons, this file is *NOT* reloaded automatically when you use
 # 'bundle exec jekyll serve'. If you change this file, please restart the server process.
 #
-# If you need help with YAML syntax, here are some quick references for you: 
+# If you need help with YAML syntax, here are some quick references for you:
 # https://learn-the-web.algonquindesign.ca/topics/markdown-yaml-cheat-sheet/#yaml
 # https://learnxinyminutes.com/docs/yaml/
 #
@@ -37,6 +37,8 @@ plugins:
 # Hide future dated posts from live blog
 future: false
 
+markdown: kramdown
+
 # Exclude from processing.
 # The following items will not be processed, by default.
 # Any item listed under the `exclude:` key here will be automatically added to

diff --git a/_includes/head.html b/_includes/head.html
@@ -0,0 +1,15 @@
+<head>
+    <meta charset="utf-8">
+    <meta http-equiv="X-UA-Compatible" content="IE=edge">
+    <meta name="viewport" content="width=device-width, initial-scale=1">
+    {%- seo -%}
+    <link rel="stylesheet" href="{{ "/assets/main.css" | relative_url }}">
+    {%- feed_meta -%}
+    {%- if jekyll.environment == 'production' and site.google_analytics -%}
+      {%- include google-analytics.html -%}
+    {%- endif -%}
+
+    {% include mathjax.html %}
+    <script async src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.7/MathJax.js?config=TeX-MML-AM_CHTML"></script>
+
+</head>
diff --git a/_includes/mathjax.html b/_includes/mathjax.html
@@ -0,0 +1,8 @@
+<script type="text/x-mathjax-config">
+    MathJax.Hub.Config({
+      tex2jax: {
+        inlineMath: [['$', '$'], ['\\(', '\\)']],
+        processEscapes: true
+      }
+    });
+</script>
diff --git a/_posts/2023-08-31-using-kani-to-validate-security-boundaries-in-aws-firecracker.md b/_posts/2023-08-31-using-kani-to-validate-security-boundaries-in-aws-firecracker.md
diff --git a/assets/images/token-bucket-diagram.png b/assets/images/token-bucket-diagram.png
diff --git a/assets/images/virtio-diagram.png b/assets/images/virtio-diagram.png