Seminar: Secure Data-Intensive Applications through Automated Formal Reasoning
Post-Doctoral Researcher, Purdue University
Monday, February 10, 2020
10:00am - 11:00am
655 McBryde Hall
Contemporary online applications are data-intensive, as opposed to compute-intensive, and run on top of large-scale inter-connected systems, such as geo-distributed databases. The high complexity of these systems coupled with ever-increasing expectations of performance and availability has made it hard for programmers to ensure the integrity of data-intensive applications, resulting in serious safety violations in applications ranging from e-commerce to cryptocurrencies.
In this talk, I demonstrate how techniques rooted in Programming Language Theory and Automatic Formal Reasoning can help developers ensure the integrity of data-intensive applications without compromising their runtime performance. First among such techniques is a method to automatically reason about the safety of non-serializable transactions, which are often used in lieu of ACID serializable transactions for their performance benefits. I show that the semantics of non-serializable transactions, albeit non-standard, can be formally related to the high-level semantics of a database application, making it possible to reason about application safety in the absence of ACID guarantees. Next, I extend the formal reasoning methodology to “weakly-consistent” geo-distributed databases that underlie modern large-scale web services, such as Amazon. I present a bounded symbolic execution technique that is effective at identifying possible safety violations in distributed database applications, while also computing possible fixes.
Finally, I present a synthesis technique that can automatically transform ordinary sequential data structures in to a class of distributed data structures called Mergeable Replicated Data Types (MRDTs) that can be composed to build linearly-scalable distributed applications. Together, the aforementioned techniques constitute a principled approach towards developing data-intensive applications with strong safety guarantees. I will end the talk with a discussion on exciting possibilities of applying formal reasoning techniques to enforce strong guarantees on the emerging class of applications, such as planet-scale decentralized applications with unconventional failure modes.
Gowtham Kaki is a post-doctoral researcher at Purdue University. He completed his Ph.D at Purdue in August 2019 under the supervision of Prof. Suresh Jagannathan. His research is at the intersection of Programing Languages, Databases, and Distributed Systems, and is focused on applying methodologies pioneered in the former domain to solve practical problems in the latter two. He received several recognitions for his work, including Google’s PhD Research Fellowship (2018), Purdue’s Maurice H. Halstead Award (2018), and his alma mater BITS Pilani’s 30-under-30 award (2019).