Probabilistic Noninterference in a Concurrent Language
Abstract
In (15) 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 high guard executes atomically The proof uses the concept of a probabilistic state of a computation following the work of Kozen [10]1.
Description
Proceedings of Fourteenth Computer Security Applications Conference
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.Related items
Showing items related by title, author, creator and subject.
-
Aluminum 7075-T6 fatigue data generation and probabilistic life prediction formulation
Kemna, John G. (Monterey, California. Naval Postgraduate School, 1998-09-01);The life extension of aging fleet aircraft requires an assessment of the safe-life remaining after refurbishment. Risk can be estimated by conventional deterministic fatigue analysis coupled with a subjective factor of ... -
Applying ensemble prediction systems to Department of Defense operations
Cunningham, Jeffrey G. (Monterey, California. Naval Postgraduate School, 2006-03);Based on recent advances, skilled objectively-determined probabilistic forecasts of some weather phenomena may be provided to operational decision-makers. Objective probabilistic forecasts that are generated from ensemble ... -
Evaluation and extensions of the probabilistic multi-hypothesis tracking algorithm to cluttered environments
Hutchins, Robert G.; Dunham, D. T. (Monterey, California. Naval Postgraduate School, 1998-01); NPS-EC-98-015This research examines the probabilistic multi-hypothesis tracker (PHMT), a batch mode, empirical, Bayesian data association and tracking algorithm. Like a traditional multi-hypothesis tracker (MHT), track estimation is ...