Skip to main content
Open Access Publications from the University of California

UC Berkeley

UC Berkeley Electronic Theses and Dissertations bannerUC Berkeley

Abstract Semantics for Software Security Analysis


Program analysis and formal methods have enabled advanced automatic software security analysis such as security policy enforcement and vulnerability discovery. However, due to the complexity of the modern software, recent applications of such techniques exhibit serious usability and scalability problems. In this thesis, we address these problems using

automatically or semi-automatically constructed abstract program semantics. Specifically, we study two typical scenarios where the power of formal techniques is limited by the problems above, and develop novel techniques that address these issues. First, we propose a new

algorithm to construct event-based program abstraction, and check contextual security policies under this abstraction. Our approach addresses the usability and scalability problems in the model-checking of security policies in event-driven programs. Second, we propose a synthesis-based algorithm to learn and check web server logic without having access to the

server-side source code. The key insight is that the client-side behavior reflects partially the server-side logic, thus we infer server-side logic by observing the client-side’s execution. We develop a declarative language to encode our domain specific modeling of common server-side operations, as well as an efficient algorithm to synthesize a server model in that language. In summary, we demonstrate that abstract semantics can bridge the gap between the human and the massive details of the program, and make formal techniques applicable in a large scale.

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View