Center for Global Studies

View Full Calendar

Formally verifying the functional correctness of Path Oblivious RAM & Enhancing Coverage-Guided Fuzzing via Phantom Program

Event Type
Seminar/Symposium
Sponsor
The Department of Computer Science, University of Illinois and FM/SE Seminar
Location
Siebel 0218
Virtual
wifi event
Date
Apr 5, 2024   2:00 pm  
Speaker
Hannah Liang, UIUC & Elen Chatikyan, UIUC
Contact
Isha Chaudhary
E-Mail
isha4@illinois.edu
Views
11
Originating Calendar
Computer Science Speakers Calendar

Talk 1

Abstract: Oblivious RAM is a class of randomized algorithms that break the association between a program’s memory access pattern and that program’s data. Path Oblivious RAM is a specific ORAM algorithm that is both theoretically interesting and practically efficient. This talk describes our plans to verify the functional correctness Path ORAM in Coq, and discusses the design decisions and tradeoffs involved. 

References: https://dependenttyp.es/pdf/oramproposal.pdf 

Talk 2

Abstract: For coverage-guided fuzzers, many of their adopted seeds are usually underused by exploring limited program states since essentially all their executions have to abide by rigorous program dependencies while only limited seeds are capable of accessing dependencies. Moreover, even when iteratively executing such limited seeds, the fuzzers have to repeatedly access the covered program states before uncovering new states. Such facts indicate that exploration power on program states of seeds has not been sufficiently leveraged by the existing coverage-guided fuzzing strategies. To tackle these issues, we propose a coverage-guided fuzzer, namely MirageFuzz, to mitigate the program dependencies when executing seeds for enhancing their exploration power on program states. Specifically, MirageFuzz first creates a “phantom” program of the target program by reducing its program dependencies corresponding to conditional statements while retaining their original semantics. Accordingly, MirageFuzz performs dual fuzzing, i.e., the source fuzzing to fuzz the original program and the phantom fuzzing to fuzz the phantom program simultaneously. Then, MirageFuzz applies the taint-based mutation mechanism to generate a new seed by updating the target conditional statement of a given seed from the source fuzzing with the corresponding condition value derived by the phantom fuzzing. To evaluate the effectiveness of MirageFuzz, we build a benchmark suite with 18 projects commonly adopted by recent fuzzing papers, and select seven open-source fuzzers as baselines for performance comparison with MirageFuzz. The experiment results suggest that MirageFuzz outperforms our baseline fuzzers from 13.42% to 77.96% averagely. Furthermore, MirageFuzz exposes 29 previously unknown bugs where 4 of them have been confirmed and 3 have been fixed by the corresponding developers. 

References: https://shadowmydx.github.io/papers/fse2023a.pdf 

link for robots only