报告题目：High-level Information Flow Policies for Secure Composition of Mutually Untrusted Codebases

报 告 人：张辰一 副教授

主 持 人：李钦 副教授

报告时间：2018年8月2日  周四  15:00-17:00

报告地点：中北校区理科楼B1002会议室

报告人简介：

张辰一，2008年毕业于新南威尔士大学，曾工作于卢森堡大学、昆士兰大学、甲骨文实验室（Oracle Labs），2016年底起任职于暨南大学信息科学技术学院计算机科学系。研究方向包括形式化方法、计算机安全和静态程序分析。

报告摘要：

Modern programming languages are designed for Internet applications and extensible systems. Code downloaded from different sources over the Internet can be composed and executed in the same process, alongside sensitive system code.

Because developers of the downloaded code may not be trusted, in order to prevent unauthorized interference across different codebases, users or deployers must grant untrusted code only those privileges that are essential to perform its intended function. This calls for a new security model that provides high-level security specification for users to authorize codebases.

In this work collaborated with Oracle Labs, we introduce a security model for capturing information-based security intentions in programs that are composed of mutually untrusted code. It makes a compositional reasoning principle to cleanly specify and enforce that different codebases with their own security requirements must be mutually satisfied by their granted privileges. We formally study a generalized form of the security model in a core object-oriented language and propose a new noninterference theorem that offers more flexible information flow relations induced by security policies that do not have to be transitive. To demonstrate such a model can be enforced statically at compile-time, we present a security type system and prove its noninterference property. Unlike traditional security types that use subtyping (of security labels) to regulate transitive information propagations in the program, our type system escapes strong transitivity by tracking the history of information flows in the program and ensuring they respect specified nontransitive policies.