BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Events - ECPv6.15.20//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Events
X-ORIGINAL-URL:https://events.ucsc.edu
X-WR-CALDESC:Events for Events
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:America/Los_Angeles
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:20240310T100000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:20241103T090000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:20250309T100000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:20251102T090000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:20260308T100000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:20261101T090000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Los_Angeles:20251119T110000
DTEND;TZID=America/Los_Angeles:20251119T121500
DTSTAMP:20260428T213708
CREATED:20251105T220936Z
LAST-MODIFIED:20251118T181912Z
UID:10005101-1763550000-1763554500@events.ucsc.edu
SUMMARY:CSE Colloquium - Flux: Refinement Types for Verified Rust Systems
DESCRIPTION:Presenter: Ranjit Jhala\, UCSD\n\nAbstract: Rust has risen as a language of choice for new systems code — from OS kernels to hypervisors\, firmware and run-times — as it is memory safe and provides the sort of abstractions needed for efficient low-level systems implementation. We present Flux\, a refinement type checker for Rust that shows how logical refinements can work in tandem with Rust’s ownership mechanisms to yield ergonomic type-based verification of low-level systems code. We then present a case study showing how Flux was used to formally verify process isolation in Tock: a microcontroller OS used in security-critical systems like the Google Security Chip (GSC) and Microsoft’s Pluton security processor. Our verification effort unearthed multiple subtle bugs that broke isolation\, allowing malicious applications to compromise the OS to potentially steal sensitive data or brick or take control of the OS. We describe how Flux helped design and implement a new granular process abstraction that is both simpler\, more efficient\, and yields formally verified security guarantees.\n\nBio:\nRanjit Jhala is a professor of Computer Science and Engineering at the University of California\, San Diego. He works on algorithms and tools that help engineer reliable computer systems. His work draws from and contributes to the areas of Model Checking\, Program Analysis\, and Automated Deduction\, and Type Systems. He helped create several influential and award winning systems including the BLAST software model checker and Liquid Types\, received ACM SIGPLAN’s Robin Milner Young Researcher Award\, and is a Fellow of the ACM.\n\nHosted by: Professor Mohsen Lesani\n\nLocation: Engineering 2\, Room E2-180\n*Refreshments such as coffee and pastries will be provided.\n\nZoom: https://ucsc.zoom.us/j/93445911992?pwd=YkJ2TQtF79h0PcNXbEcpZLbpK0coiY.1
URL:https://events.ucsc.edu/event/cse-colloquium-flux-refinement-types-for-verified-rust-systems/
LOCATION:Engineering 2\, Engineering 2 1156 High Street\, Santa Cruz\, CA\, 95064
CATEGORIES:Lectures & Presentations
ATTACH;FMTTYPE=image/jpeg:https://events.ucsc.edu/wp-content/uploads/2025/11/235.jpg
GEO:37.0009723;-122.0632371
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=Engineering 2 Engineering 2 1156 High Street Santa Cruz CA 95064;X-APPLE-RADIUS=500;X-TITLE=Engineering 2 1156 High Street:geo:-122.0632371,37.0009723
END:VEVENT
END:VCALENDAR