Accession Number:

ADA495086

Title:

Probabilistic Noninterference in a Concurrent Language

Descriptive Note:

Proceedings paper

Corporate Author:

NAVAL POSTGRADUATE SCHOOL MONTEREY CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1999-08-19

Pagination or Media Count:

23.0

Abstract:

In previous work 16, we give a type system that guarantees that well-typed multi-threaded programs are possibilistically noninterfering. If thread scheduling is probabilistic, however, then well-typed programs may have probabilistic timing channels. We describe how they can be eliminated without making the type system more restrictive. We show that well-typed concurrent programs are probabilistically noninterfering if every total command with a guard containing high variables executes atomically. The proof uses the notion of a probabilistic state of a computation from Kozens work in the denotational semantics of probabilistic programs 11.

Subject Categories:

  • Computer Programming and Software
  • Computer Systems Management and Standards

Distribution Statement:

APPROVED FOR PUBLIC RELEASE