From b181e467e8ee16dea70d1d5ce6f35757d7678caf Mon Sep 17 00:00:00 2001 From: gshen42 Date: Tue, 16 Apr 2024 22:22:01 +0000 Subject: [PATCH] regenerate after: Update Ismail's talk info --- index.xml | 20 +++++++++++++++++--- lsd-seminar/2024sp/index.html | 20 +++++++++++++++++--- themes/academic | 1 - 3 files changed, 34 insertions(+), 7 deletions(-) delete mode 160000 themes/academic diff --git a/index.xml b/index.xml index 08e9e99..9069be1 100644 --- a/index.xml +++ b/index.xml @@ -52,9 +52,9 @@ </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> @@ -137,6 +137,20 @@ <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/lsd-seminar/2024sp/index.html b/lsd-seminar/2024sp/index.html index cf51dd0..d46df16 100644 --- a/lsd-seminar/2024sp/index.html +++ b/lsd-seminar/2024sp/index.html @@ -233,9 +233,9 @@

Languages, Systems, and Data Seminar (Spring 2024)

-April 19 -Kuru Ismail -TBD +April 19 +Ismail Kuru +Modal Abstractions for Virtualizing Memory Addresses @@ -318,6 +318,20 @@

April 12

Bio: 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.

+

April 19

+ +

Speaker: Ismail Kuru

+ +

Title: Modal Abstractions for Virtualizing Memory Addresses

+ +

Abstract: 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’s memory management’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.

+ +

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.

+ +

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.

+ +

Bio: 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.

+

Archive

diff --git a/themes/academic b/themes/academic deleted file mode 160000 index 8d596ff..0000000 --- a/themes/academic +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 8d596ffed2d080010c561679cf4e9b4da1554781