The JE Programming Language

What is JE?

JE is a programming language to develop secure enclave applications.
JE provides high-level abstractions to specify the code to be placed inside the enclaves and different privacy levels for data objects. The static type system checks information flow and guarantees that the secret data is not leaked outside the enclave.

Background

Confidential computing is a promising technology for securing code and data-in-use on untrusted host machines, e.g., the cloud. Many hardware vendors offer the confidential computing services using Trusted Execution Environments (TEEs). A TEE is a hardware protected execution environment that allows performing confidential computations over sensitive data on untrusted hosts. Despite the appeal of achieving strong security guarantees against low-level attackers, two challenges hinder the adoption of TEEs. First, developing software in high-level managed languages, e.g., Java or Scala, taking advantage of existing TEEs is complex and error-prone. Second, partitioning an application into components that run inside and outside a TEE may break application-level security policies, resulting in an insecure application when facing a realistic attacker.

JE tries to address both these challenges. JE is a programming model that integrates a TEE, abstracting away low-level programming details such as initialization and loading of data into the TEE. JE only requires developers to add annotations to their programs to enable the execution within the TEE. It has a security type system that checks confidentiality and integrity policies against realistic attackers with full control over code running outside the TEE. Presently, JE works with Intel SGX as a target TEE.

For the formal details of the type-system and security guarantees, have a look at our paper.

A sample JE code

public class NonEnclaveMain {

    public static void main(String[] args) {
        Boolean result = PasswordChecker.checkPassword("abc");
    }
}
@Enclave
class PasswordChecker {
	@Secret
	private static String password;
		
	@Gateway
	public static Boolean checkPassword(String guess) {
		return declassify(password.equals(guess));
	} 
}

The two snippets show a simple password checker application with two classes. The NonEnclaveMain class is to be placed outside the enclave and the PasswordChecker class (annotated with the @Enclave annotation) inside the enclave. The @Enclave, @Secret and @Gateway annotations and the declassify method are the JE abstractions. The class-level @Enclave annotation denotes that the annotated class is to be placed inside the enclave. The field-level @Secret annotation denotes secret fields whose values must not leak outside the SGX enclave. The @Gateway annotation specifies that the annotated methods are accessible from the non-enclave environment.

Try it out

You can find the instructions to install and run JE here. A simple JE encryptor program can be compiled and verified using the JE compiler. Instructions for automatic deployment into Intel SGX will be added soon !!!

Contact

Aditya Oak

Publications

Credits

JE is a project developed at the Technical University of Darmstadt, the University of St. Gallen and the KTH Royal Institute of Technology.

Contributors

Supported by