|
|
Abstract:
In language-based security, confidentiality and integrity policies
conveniently specify the permitted flows of information between
different parts of a program with diverse levels of trust.
These policies enable a simple treatment of security, and they can
often be verified by typing. However, their enforcement in concrete
systems involves delicate compilation issues.
We consider cryptographic enforcement mechanisms
for imperative programs with untrusted components.
Such programs may represent, for instance, distributed systems
connected by some untrusted network.
In source programs, security depends on an abstract access-control
policy for reading and writing the shared memory. In their
implementations, shared memory is unprotected and security depends
instead on encryption and signing.
We build a translation from well-typed source programs and policies
to cryptographic implementations. To establish its correctness, we
develop a type system for the target language. typing rules enforce a
correct usage of cryptographic primitives against active adversaries;
from an information-flow viewpoint, they capture controlled forms of
robust declassification and endorsement. We show type soundness for a
variant of the non-interference property, then show that our
translation preserves typability.
We rely on concrete primitives and hypotheses for cryptography,
stated in terms of probabilistic polynomial-time algorithms and
games. We model these primitives as commands in our target language.
Thus, we develop a uniform language-based model of security, ranging
from computational non-interference for probabilistic programs down to
standard cryptographic hypotheses.
The article can be found
there.
|