regenerate after: Update Ismail's talk info

lsd-ucsc · Apr 16, 2024 · b181e46 · b181e46
1 parent 811308d
commit b181e46
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 7 deletions.
diff --git a/index.xml b/index.xml
@@ -52,9 +52,9 @@
 &lt;/tr&gt;
 
 &lt;tr&gt;
-&lt;td&gt;April 19&lt;/td&gt;
-&lt;td&gt;Kuru Ismail&lt;/td&gt;
-&lt;td&gt;&lt;em&gt;TBD&lt;/em&gt;&lt;/td&gt;
+&lt;td&gt;&lt;a href=&#34;#april-19&#34;&gt;April 19&lt;/a&gt;&lt;/td&gt;
+&lt;td&gt;Ismail Kuru&lt;/td&gt;
+&lt;td&gt;Modal Abstractions for Virtualizing Memory Addresses&lt;/td&gt;
 &lt;/tr&gt;
 
 &lt;tr&gt;
@@ -137,6 +137,20 @@
 
 &lt;p&gt;&lt;strong&gt;Bio:&lt;/strong&gt; Dan works as a postdoc at the University of Southern Denmark and is receiving his PhD from the University of Illinois at Urbana-Champaign (UIUC). He is the author of the UIGC library for Akka, which provides fault-tolerant resource management for distributed actor systems. Dan’s research focuses on making distributed reactive applications easier to write and reason about.&lt;/p&gt;
 
+&lt;h2 id=&#34;april-19&#34;&gt;April 19&lt;/h2&gt;
+
+&lt;p&gt;&lt;strong&gt;Speaker:&lt;/strong&gt; Ismail Kuru&lt;/p&gt;
+
+&lt;p&gt;&lt;strong&gt;Title:&lt;/strong&gt; Modal Abstractions for Virtualizing Memory Addresses&lt;/p&gt;
+
+&lt;p&gt;&lt;strong&gt;Abstract:&lt;/strong&gt; Virtual Memory Managers are critical pieces of general-purpose OS kernels. They enable virtualizing the addresses of memory regions by realizing the address translation mechanism using CPU&amp;rsquo;s memory management&amp;rsquo;s (MMU) kernel-controlled page tables. Operating systems manipulate these virtualized memory mappings to isolate untrusted processes, restrict which memory is accessible to different processes, hide memory limits from user programs, etc.&lt;/p&gt;
+
+&lt;p&gt;Unfortunately, verifying them becomes challenging as they are interfaced by the complex hardware: the page tables are updated via writes to those memory locations, using addresses that are themselves virtualized!  Prior work on verification of VMM has either only handled a single address space, trusted significant pieces of assembly code, or resorted to direct reasoning over machine semantics rather than exposing a clean logical interface.&lt;/p&gt;
+
+&lt;p&gt;In this talk, I will be explaining the logical abstractions, some of which are inspired by Hybrid Logic and allow us to mention resources (virtualized memory addresses) belonging to different address spaces within the same specification.&lt;/p&gt;
+
+&lt;p&gt;&lt;strong&gt;Bio:&lt;/strong&gt; I am Ismail Kuru, a final year PhD student at Drexel University, and I am advised by Dr. Colin S. Gordon. Right before coming to Drexel, I was a senior software engineer at CRYTEK Gaming Company. Before then, I had finished my computer science masters courses at TU Munich and graduated with an M.S. degree from Koc University as a Microsoft Research EMEA scholar for graduate studies.&lt;/p&gt;
+
 &lt;hr /&gt;
 
 &lt;p&gt;&lt;a href=&#34;../&#34;&gt;Archive&lt;/a&gt;&lt;/p&gt;

diff --git a/lsd-seminar/2024sp/index.html b/lsd-seminar/2024sp/index.html
@@ -233,9 +233,9 @@ <h1 itemprop="name">Languages, Systems, and Data Seminar (Spring 2024)</h1>
 </tr>
 
 <tr>
-<td>April 19</td>
-<td>Kuru Ismail</td>
-<td><em>TBD</em></td>
+<td><a href="#april-19">April 19</a></td>
+<td>Ismail Kuru</td>
+<td>Modal Abstractions for Virtualizing Memory Addresses</td>
 </tr>
 
 <tr>
@@ -318,6 +318,20 @@ <h2 id="april-12">April 12</h2>
 
 <p><strong>Bio:</strong> Dan works as a postdoc at the University of Southern Denmark and is receiving his PhD from the University of Illinois at Urbana-Champaign (UIUC). He is the author of the UIGC library for Akka, which provides fault-tolerant resource management for distributed actor systems. Dan’s research focuses on making distributed reactive applications easier to write and reason about.</p>
 
+<h2 id="april-19">April 19</h2>
+
+<p><strong>Speaker:</strong> Ismail Kuru</p>
+
+<p><strong>Title:</strong> Modal Abstractions for Virtualizing Memory Addresses</p>
+
+<p><strong>Abstract:</strong> Virtual Memory Managers are critical pieces of general-purpose OS kernels. They enable virtualizing the addresses of memory regions by realizing the address translation mechanism using CPU&rsquo;s memory management&rsquo;s (MMU) kernel-controlled page tables. Operating systems manipulate these virtualized memory mappings to isolate untrusted processes, restrict which memory is accessible to different processes, hide memory limits from user programs, etc.</p>
+
+<p>Unfortunately, verifying them becomes challenging as they are interfaced by the complex hardware: the page tables are updated via writes to those memory locations, using addresses that are themselves virtualized!  Prior work on verification of VMM has either only handled a single address space, trusted significant pieces of assembly code, or resorted to direct reasoning over machine semantics rather than exposing a clean logical interface.</p>
+
+<p>In this talk, I will be explaining the logical abstractions, some of which are inspired by Hybrid Logic and allow us to mention resources (virtualized memory addresses) belonging to different address spaces within the same specification.</p>
+
+<p><strong>Bio:</strong> I am Ismail Kuru, a final year PhD student at Drexel University, and I am advised by Dr. Colin S. Gordon. Right before coming to Drexel, I was a senior software engineer at CRYTEK Gaming Company. Before then, I had finished my computer science masters courses at TU Munich and graduated with an M.S. degree from Koc University as a Microsoft Research EMEA scholar for graduate studies.</p>
+
 <hr />
 
 <p><a href="../">Archive</a></p>

diff --git a/themes/academic b/themes/academic