All seminars will take place on Fridays at 11 a.m. in DBH 6011. Check seminar details below.
October 7, 2022
11:00am - 12:00pm
Synthesis and Verification of Distributed Systems
Distributed systems are the backbone of modern computing. Yet, building distributed systems with reliability and security guarantees has proven to be complicated, and remains elusive. The complication is not only faced by experts that design and implement distributed systems but is also exposed to client programmers that develop distributed applications. This talk presents an overview of our cross-stack research on mechanized verification for distributed middleware, and automatic coordination synthesis for client applications. We will then present our recent project that, in the face of attacks, assures end-to-end policies for the three aspects of trustworthiness: confidentiality, integrity and availability. Inter-organizational systems where subsystems with partial trust need to cooperate are common in healthcare, finance and military. We present the Hamraz synthesis tool that given a class and the specification of its end-to-end policies as types, applies type inference to automatically place and replicate the fields and partitioned methods of the class on Byzantine quorum systems, and synthesizes trustworthy-by-construction distributed systems. The type system provably guarantees that well-typed methods enjoy noninterference for the three properties, and that their types quantify their resilience to Byzantine attacks. The experiments show the resiliency of the resulting systems; they can gracefully tolerate attacks that are as strong as the specified policies.
Mohsen Lesani is an associate professor at the Computer Science and Engineering department of the University of California, Riverside. He spent his postdoc at MIT and obtained his PhD from UCLA. His research interests are reliability and security of software systems especially concurrent and distributed systems. He received the NSF CAREER award in 2020 and the DARPA YFA in 2022. His research has been recognized as SIGPLAN Research Highlight in 2019 and received the distinguished paper award at OOPSLA '18.