可组合的描述符泄露类型检查  

Compositional Type Checking of Descriptor Leaking

作　　者：李沁[1] 缪瑨 

机构地区：[1]安徽工业大学计算机科学与技术学院,马鞍山243032

出　　处：《计算机科学》2015年第10期184-188,共5页Computer Science

基　　金：国家自然科学基金(61170070);省教育厅科研项目(kj2012Z022);国家科技支撑计划(2012BAK30B049-02);安徽高校省级自然科学研究重大项目(KJ2014ZD05)资助

摘　　要：应用程序通过操作系统的系统调用对文件描述符进行操作并管理文件资源。如果应用程序对资源描述符的管理出现错误并发生描述符泄漏,会严重影响系统的可用性。据此,提出了一种检查程序是否会导致描述符泄漏的类型系统,给出了描述符操作方法的语义和类型约束,证明了类型系统的可靠性定理。此外,还初步讨论了该类型系统在并发程序下的扩展。Programs manage files, as a kind of resource, using system calls provided by operating systems to manipulate file descriptors. The availability of the system will be significantly degenerated if programs deal with file descriptors ar- bitrarily. We proposed a type system to check whether a program leaks some resource （typically, file） descriptors. We defined semantics for descriptor-related operations in sequential programs, and proved that the type system is sound with respect to our semantics. In addition, the extension of this type system with concurrent semantics was discussed.

关 键 词：描述符泄露 类型检查 软件安全 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]