|
Inter-organizational
systems where subsystems with partial trust need to cooperate are
common in healthcare, finance and military. In the face of malicious
Byzantine attacks, the ultimate goal is to assure end-to-end policies
for the three aspects of trustworthiness: confidentiality, integrity
and availability. In contrast to confidentiality and integrity,
provision and validation of availability has been often sidestepped.
This paper guarantees end-to-end policies simultaneously for all the
three aspects of trustworthiness. It presents a security-typed
object-based language, a partitioning transformation, an operational
semantics, and an information flow type inference system for
partitioned and replicated classes. The type system provably guarantees
that well-typed methods enjoy noninterference for the three properties,
and that their types quantify their resilience to Byzantine attacks.
Given a class and the specification of its end-to-end policies, the
Hamraz tool applies type inference to automatically place and replicate
the fields and methods of the class on Byzantine quorum systems, and
synthesize trustworthy-by-construction distributed systems. The
experiments show the resiliency of the resulting systems; they can
gracefully tolerate attacks that are as strong as the specified
policies.
|
|