Contextual refinement is a compositional approach to compositional verification of concurrent objects. There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification. However, these program logics for contextual refinement verification cannot support objects with resource ownership transfer, which is a common pattern in many concurrent objects, such as the memory management module in OS kernels, which transfers the allocated memory block between the object and clients. In this paper, we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership transfer. We also design a program logic to verify contextual refinement of concurrent objects w.r.t. their abstract specifications. We have successfully applied our logic to verifying an implementation of the memory management module, where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.

Inline assembly code is common in system software to interact with the underlying hardware platforms. The safety and correctness of the assembly code is crucial to guarantee the safety of the whole system. In this paper, we propose a practical Hoare-style program logic for verifying SPARC (Scalable Processor Architecture) assembly code. The logic supports modular reasoning about the main features of SPARCv8 ISA (instruction set architecture), including delayed control transfers, delayed writes to special registers, and register windows. It also supports relational reasoning for refinement verification. We have applied it to verify that there is a contextual refinement between a context switch routine in SPARCv8 and a switch primitive. The program logic and its soundness proof have been mechanized in Coq.

Inter-process communication (IPC) provides a message passing mechanism for information exchange between applications. It has been long believed that IPCs can be abused by malware writers to launch collusive information leak using two or more applications. Much work on privacy protection focuses on the simple information leak caused by the individual applications and lacks effective approaches to preventing the collusive information leak caused by IPCs between multiple processes. In this paper, we propose a hybrid approach to prevent the collusive information leak based on information flow control. Our approach combines static information flow analysis and dynamic runtime checking together. Information leak caused by individual processes is prevented through static information flow control, and dynamic checking is done at runtime to prevent the collusive information leak. Such a combination may effectively reduce the runtime overhead of pure dynamic checking, and reduce false-alarms in pure static analysis. We develop this approach based on an abstract and simplified programming model, and formalize a novel definition of the leak-freedom property as our target security property. A simulation-based proof technique is used to prove that our approach is able to guarantee leak-freedom. All proofs are mechanized in Coq.