Computer Science ›› 2015, Vol. 42 ›› Issue (10): 184-188.

Previous Articles     Next Articles

Compositional Type Checking of Descriptor Leaking

LI Qin and MIAO Jin   

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

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

[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

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!