Announcing the Final Examination of

Tianyu Chen

for the Degree of Doctor of Philosophy in Computer Science

Friday, May 2, 2025, 10:00am

Luddy Hall Room 1106 Dorsey Auditorium

The Holy Grail of Gradual Security

Ensuring the security and privacy of personal data typically involves tracking and checking the flow of information. Languages with gradual information-flow control combine static and dynamic techniques to prevent security leaks. Gradual languages should satisfy the gradual guarantee: programs that only differ in the precision of their type annotations should behave the same modulo cast errors. Unfortunately, Toro et al. [2018] identify a tension between the gradual guarantee and information security. They conjecture that it is not possible to enforce noninterference and satisfy the gradual guarantee.

In my PhD dissertation, I harmoniously combine static and dynamic enforcement of information-flow control (IFC) in one programming language, λIFCStar. λIFCStar satisfies both noninterference and the gradual guarantee at the same time without making any sacrifices. λIFCStar (1) enforces information flow security, (2) satisfies the gradual guarantee, (3) supports type-based reasoning, and (4) requires no extra static analysis prior to program execution. The key to the design of λIFCStar is to exclude the unknown label from runtime security labels. On the technical side, the semantics of λIFCStar is the first gradual information-flow control language to be specified using coercion calculi (a la Henglein). Casts in λIFCStar are represented by security coercions, which enforce the flow of information while satisfying the gradual guarantee.

I mechanize the proofs of type safety and the gradual guarantee for λIFCStar in the Agda proof assistant. I prove noninterference for λIFCStar by simulating λIFCStar with its dynamic extreme. 

In summary, my thesis is that it is possible to design a gradual IFC programming language that satisfies noninterference and the gradual guarantee while supporting type-based reasoning, by excluding the unknown label from run-time security labels and using security coercions to represent casts.

Outline of Current Studies                                                                           

Major: Computer Science, Programming Languages

Minor(s): Computer Science

Educational Career

Bachelor of Engineering, Computer Science and Technology, Tsinghua University, China, 2016

Committee in Charge

Professor Jeremy Siek, Director of Center for Programming Systems, Chairperson, (812) 855-7241, Computer Science

Professor Amr Sabry, (812) 855-3668, Computer Science

Associate Professor Chung-chieh Shan, Computer Science

Associate Professor Sam Tobin-Hochstadt, Director of Undergraduate Studies for Computer Science, Computer Science

Any member of the Graduate Faculty may attend.  As a courtesy, please notify the committee chairperson in advance.

Best Wishes,
Tracy Hollon
Student Services Coordinator

Graduate Services Office, Luddy School of Informatics, Computing, and Engineering 

Indiana University Bloomington 

Phone: 812-855-4841 

Email: tahollon@iu.edu 
Office: 1119 Luddy Hall