Trustworthy computing systems must provide data confidentiality and data integrity, and must be available. This paper shows that these security properties can be provided by construction, by compiling high-level, security-typed source code into explicitly distributed, security-typed target code. This code transformation provably preserves the confidentiality, integrity, and availability properties of the source. A key technical contribution is the new target language, which describes distributed computation. In this language, any well-typed program satisfies noninterference properties that ensure confidentiality and integrity. Further, the language supports the distribution and replication of code and data using quorum replication, which enables simultaneous enforcement of integrity and availability. A novel timestamp scheme handles out-of-order accesses by concurrent distributed threads without creating covert channels.