Information flow properties are a way of specifying security
properties of systems. A system is viewed as generating traces
containing "confidential" and "visible" events (only the latter
being observable by a "low-level" user) and the information flow
properties specify restrictions on the kind of traces the system
may generate, so as to restrict the amount of information a
low-level user can infer about confidential events having taken
place (or not) in an execution. Mantel identifies "basic security
predicates" or BSPs and shows them to be the building blocks of
most of the known trace-based properties in the literature.
Traditionally BSPs have been reasoned about via unwinding
conditions that capture whether a system satisfies a particular
BSP. First, we show that the checking of unwinding conditions can
be simplified to checking conditions on a maximal simulation
relation. Second, we show that the BSPs can be characterized in
terms of regularity preserving language-theoretic operations. This
leads to a decision procedure for checking whether a finite state
system satisfies a given BSP. Finally, we prove that the problem of
verifying BSPs for pushdown systems is undecidable.
General
Is the information for this product incomplete, wrong or inappropriate?
Let us know about it.
Does this product have an incorrect or missing image?
Send us a new image.
Is this product missing categories?
Add more categories.
Review This Product
No reviews yet - be the first to create one!