PhD Proposal: Synthesis of Web Apps through Lightweight Abstractions

Sankha Guria
12.02.2021 09:00 to 11:00

IRB 5105

Program synthesis promises to enable programmers to automatically write correct by construction code from higher level specifications. A large class of synthesis tools has become mainstream for domains such as bitvector or integer programs, spreadsheet manipulation, and even data visualization. However, this rise in popularity has highlighted the problem of scaling such tools to bigger applications. This dissertation proposal investigates if synthesis tools for web applications can be built by systematically lifting language constructs to formal abstractions where feasible, while using tests to ensure synthesized programs remain bug-free.First, we present a verified framework to enforce quantitative security policies, for data declassification in Haskell web apps. Here synthesis is used to automatically generate optimal posterior knowledge for a sensitive computation directly guided by refinement types. Then, we present a tool to automatically synthesize database access methods for Ruby on Rails applications by using lightweight type-and-effect labels of library methods to guide the search, and tests to ensure correctness. Together, these tools demonstrate the use of synthesis to make two important aspects of web apps easy: security and database access.Finally, we present plans to extend this work to a general abstract interpretation framework that combines formal user-specified guarantees with correctness via tests. We plan to show the general applicability of the framework to domains such as string manipulation and Python’s dataframe transformation operations. These results aim to serve as encourage the use of abstraction-guided methods for designing practical synthesis tools.Examining Committee:

Chair:Department Representative:Members:

Dr. David Van Horn Dr. Hal DauméDr. Jeffrey S. FosterDr. Michael Hicks