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

计算机科学 ›› 2015, Vol. 42 ›› Issue (10): 184-188.

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

李沁,缪瑨

安徽工业大学计算机科学与技术学院马鞍山243032,安徽工业大学计算机科学与技术学院马鞍山243032

出版日期:2018-11-14 发布日期:2018-11-14
基金资助:
本文受国家自然科学基金(61170070),省教育厅科研项目(kj2012Z022),国家科技支撑计划(2012BAK30B049-02),安徽高校省级自然科学研究重大项目(KJ2014ZD05)资助

Compositional Type Checking of Descriptor Leaking

LI Qin and MIAO Jin

Online:2018-11-14 Published:2018-11-14

摘要/Abstract

摘要： 应用程序通过操作系统的系统调用对文件描述符进行操作并管理文件资源。如果应用程序对资源描述符的管理出现错误并发生描述符泄漏,会严重影响系统的可用性。据此,提出了一种检查程序是否会导致描述符泄漏的类型系统,给出了描述符操作方法的语义和类型约束,证明了类型系统的可靠性定理。此外,还初步讨论了该类型系统在并发程序下的扩展。

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

Abstract: 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 arbitrarily.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.

Key words: Descriptor leaking,Type checking,Software safety

李沁,缪瑨. 可组合的描述符泄露类型检查[J]. 计算机科学, 2015, 42(10): 184-188. https://doi.org/

LI Qin and MIAO Jin. Compositional Type Checking of Descriptor Leaking[J]. Computer Science, 2015, 42(10): 184-188. https://doi.org/

参考文献

[1] Albert E,et al.Resource Usage Analysis and Its Application to Resource Certification[M]∥ Aldini V A,et al.,eds.Foundations of Security Analysis and Design.Springer Berlin Heidelberg,2009,5705:258-288
[2] Albert E,et al.On the Inference of Resource Usage Upper and Lower Bounds[J].ACM Trans.Comput.Logic,2013,14(3):1-35
[3] Albert E,et al.Incremental resource usage analysis[C]∥Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation.Philadelphia,Pennsylvania,USA,2012:25-34
[4] Jost S,et al.Static determination of quantitative resource usage for higher-order programs[C]∥Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.Madrid,Spain,2010
[5] Kobayashi N,et al.Resource Usage Analysis for the π-Calculus[M]∥ Verification,Model Checking,and Abstract Interpretation.Springer Berlin Heidelberg,2006:298-312
[6] Bartoletti M,et al.Local policies for resource usage analysis[J].ACM Trans.Program.Lang.Syst.,2009,31:1-43
[7] Antunes J,et al.Detection and Prediction of Resource-Exhaustion Vulnerabilities[C]∥19th International Symposium on Software Reliability Engineering,2008(ISSRE 2008).2008:87-96
[8] Calcagno C,et al.Compositional Shape Analysis by Means of Bi-Abduction[C]∥POPL’09.2009:289-300
[9] Lokuciejewski P,et al.A Fast and Precise Static Loop Analysis Based on Abstract Interpretation,Program Slicing and Polytope Models[C]∥Code Generation and Optimization,2009(CGO 2009).2009:136-146
[10] Coughlin D,et al.Fissile type analysis:Modular Checking of Almost Everywhere Invariants [J].SIGPLAN Notices,2014,49(1):73-85
[11] Pugh W,et al.Constraint-Based Array Dependence Analysis[J].ACM Transactions on Programming Languages and Systems,1998,20(3):635-678
[12] Khedker U,et al.Heap reference analysis using access graphs.http://www.cs.ox.ac.uk/seminars/584.html
[13] Hind M,et al.Interprocedural Pointer Alias Analysis[J].ACM Transactions on Programming Languages and Systems,1999,1(4):848-894

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed