Slot Games for Detecting Timing Leaks of Programs

TL;DR

This paper introduces a method using slot-game semantics to verify secure information flow in programs, focusing on detecting timing leaks that could reveal secret data through covert channels.

Contribution

It presents a novel application of slot-game semantics for quantitative security analysis, enabling automated verification of timing leak vulnerabilities in programs.

Findings

Slot-game models enable precise security analysis.

The approach accounts for both extensional and intensional properties.

Automated verification of timing leaks is feasible with this method.

Abstract

In this paper we describe a method for verifying secure information flow of programs, where apart from direct and indirect flows a secret information can be leaked through covert timing channels. That is, no two computations of a program that differ only on high-security inputs can be distinguished by low-security outputs and timing differences. We attack this problem by using slot-game semantics for a quantitative analysis of programs. We show how slot-games model can be used for performing a precise security analysis of programs, that takes into account both extensional and intensional properties of programs. The practicality of this approach for automated verification is also shown.