Candidate: Billy Bai
Date: March 27, 2025
Time: 10:00am to 12:00pm
Location: virtual meeting via Teams
Supervisor: Dr. Arie Gurfinkel
All are welcome!
Abstract:
External third-party APIs are commonly used in the real-world programming. Documentations, specifications, or protocols are given by the API designer to direct the combination of those APIs. The violation of those restrictions may not crush the program but often weaken or break the guarantees of the framework, which would be vital to some safety-critical systems such as encryption.
Typestate system is one of the approaches to check the restrictions that can be represented as a finite-state system protocol. The restrictions are encoded as a type called typestate that tracks the compliance of the protocol. However, most typestate systems rely on the alias analysis results. Therefore, the efficiency, precision, and soundness of the typestate system heavily depend on the performance of the alias analysis.
This thesis investigates the typestate system that can be soundly checked without alias information to avoid the computational expense of alias analysis, hence be checked efficiently. We identify the group of typestate systems called the accumulative typestate system, which is a superset of typestate systems that can be checked soundly without alias information. We also pin down two groups of accumulative typestate systems that can always be checked without alias information.
We formalize the notion of the protocol and the typestate system. It proves that the accumulative protocol is a necessary condition for the typestate system to be sound without alias information, and the two groups of the accumulative typestate systems are always sound without alias information.