Research On File Descriptor Leaking Based On Type Checking

File resource in operating system is operated by file descriptor when programs(or processes) accessing it. If the program for the management of file descriptor has error occurred, it may lead to resource leaks, and seriously affect system availability. We call this situation file descriptor leaking.File descriptor leaking is a kind of system resource leaking, and type checking is an important research methods of resource management. In this paper, we propose a type system for type-checking whether a program leaks some resource(typically, file)descriptors. The main work is as follows:1. The syntax model is to establish for this type system to ensure that the keywords in usual language and descriptor-related operations is contained. So any procedures relating to the descriptor can be expressed this type system.2. Then we give the semantic model of this type system. Specifically, we abstract the storage structure of descriptor that running in program(the storage structure we called it Configuration), then we observed the changes of this structure and made it in axioms. Then we give an accurate definition of the descriptor leaking formally through configuration.3. Hoare logic is used to give this type system a type axioms. Then we propose reliability theory for this type system. According to this theory,a system will not have file descriptor leaking occur if it sacrifice reliability theory.4. We given a strict mathematical proof of this reliability theory.According this type system we designed the language named REMA for static compilated program to find leaking descriptors, and we made REMA complier with Java, so that we can verify the validation of type checking by experiments.