Stateless Code Model Checking of Information Flow Security

TL;DR

This paper introduces a novel approach using stateless code model checking to verify observational determinism, a key security property for multithreaded programs, addressing limitations of traditional stateful methods.

Contribution

It is the first to apply stateless code model checking for verifying observational determinism in concurrent programs, improving scalability and testing efficiency.

Findings

Successfully verified observational determinism using stateless model checking

Demonstrated effectiveness on large, complex concurrent programs

Addressed state space explosion issues in security verification

Abstract

Observational determinism is a security property that characterizes secure information flow for multithreaded programs. Most of the methods that have been used to verify observational determinism are based on either type systems or conventional model checking techniques. A conventional model checker is stateful and often verifies a system model usually constructed manually. As these methods are based on stateful model checking, they are confronted with the state space explosion problem. In order to verify and test computer programs, stateless code model checking is more appropriate than conventional techniques. It is an effective method for systematic testing of large and complicated concurrent programs, and for exploring the state space of such programs. In this paper, we propose a new method for verifying information flow security in concurrent programs. For the first time, we use stateless code model checking to verify observational determinism.