PLDI'16

PDF

Hardware support for isolated execution (such as Intel SGX) enables development of applications that keep their code and data confidential even while running in a hostile or compromised host. However, automatically verifying that such applications satisfy confidentiality remains challenging. We present a methodology for designing such applications in a way that enables certifying their confidentiality. Our methodology consists of forcing the application to communicate with the external world through a narrow interface, compiling it with runtime checks that aid verification, and linking it with a small runtime that implements the narrow interface. The runtime includes services such as secure communication channels and memory management. We formalize this restriction on the application as Information Release Confinement (IRC), and we show that it allows us to decompose the task of proving confidentiality into (a) one-time, human-assisted functional verification of the runtime to ensure that it does not leak secrets, (b) automatic verification of the application's machine code to ensure that it satisfies IRC and does not directly read or corrupt the runtime's internal state. We present /CONFIDENTIAL: a verifier for IRC that is modular, automatic, and keeps our compiler out of the trusted computing base. Our evaluation suggests that the methodology scales to real-world applications.

Purpose

• Protect IRC: to prevent info leakage
• WCFI-RW: weak form of control-flow integrity, and along with restrictions on reads and writes
• Formally verify a set of checks to enforce WCFI-RW in SIRs
• Not to depend on a specific compiler, which is not in the TCB

Threat model

• Application U (in SIR) is not malicious but may contain bugs
• U may also use third-party libraries
• The system other than SIR is hostile/compromised

Design

• U and libraries(L) are verified separately
• U can only use L to send and recv data outside of SIR

Method

1. Establish a formal model of U's syntax
2. Define what an adversary can do under this threat model, formally
3. Define the target (confidentiality)
4. Deduce the properties required for WCFI-RW, both for applications and libraries
5. Derive and instrument checks in code
6. Verify the properties still hold.

Notice that

• These checks derived from the properties ensures WCFI-RW
• The verification may scale

Insights

• The library may also compromise the app
• No check of jump into the middle of instrumentation(s)
• Assumes the page permissions can be changed
• Only needs SP is in U???