Encifher

Symbolic Execution

What is symbolic execution and how does it works

Encifher leverages symbolic execution (execution on pointers/handles) to efficiently enable encrypted computations onchain, overcoming latency challenges by abstracting ciphertext and instead enabling computations symbolically on their handles/pointers. This reduces computational overhead within blockchain transactions and enhances system performance.

What are pointers/handles

  • Pointers/handles are 16 bytes (128 bit) value which maps a certain ciphertext.

Doing symbolic execution over pointers has many advantages:

  • The host chain does not need to change anything, run expensive operations or use specific hardware.

  • The host chain is not slowed down by encrypted computation, so non-encrypted transactions can be executed as fast as they always have been

  • Encrypted operations can be executed in parallel, rather than sequentially, dramatically increasing throughput.

Since all ciphertexts on the host chain are simply pointers (the actual data is stored offchain in a public storage layer), The operations can be chained just like regular operations, without needing to wait for the previous ones to complete. The only time we need to wait for a ciphertext to be computed is when it has to be decrypted.

From the implementation standpoint it looks something like this:

Suppose if a developer wants to add two encrypted values this is how he can do so

// here pet_executor program exposes certain method to enable various types of symbolic computation
let add_result = pet_executor::cpi::add(ctx.accounts.executor_cpi_context(signer_seeds), pointer1, pointer2)?;

Internally, it calls


// lhs: left input pointer
// rhs: right input pointer
// scalar_byte: says whether rhs is a pointer or a plaintext value

pub fn pet_add(lhs: u128, rhs: u128, scalar_byte: u8) -> Result<u128> {
    let supported_types =
        (1 << 1) + (1 << 2) + (1 << 3) + (1 << 4) + (1 << 5) + (1 << 6) + (1 << 8);
    require_type(lhs, supported_types)?;

    let lhs_type = type_of(lhs);
    let scalar = scalar_byte & 0x01;

    binary_op(Operators::PetAdd, lhs, rhs, scalar, lhs_type)
}

// further binary_op method calculate resultant handle/pointer upon addition computation over these two inputs handles 
pub fn binary_op(op: Operators, lhs: u128, rhs: u128, scalar: u8, result_type: u8) -> Result<u128> {
    if scalar == 0 {
        let type_rhs = type_of(rhs);
        let type_lhs = type_of(lhs);

        require!(type_lhs == type_rhs, ExecutorError::IncompatibleTypes);
    }

    let hash_input = [
        &[op as u8].as_slice(),
        lhs.to_le_bytes().as_slice(),
        rhs.to_le_bytes().as_slice(),
        &[scalar].as_slice(),
    ]
    .concat();

    let hash = hash::hash(&hash_input);
    let result = u128::from_le_bytes(hash.to_bytes()[0..16].try_into().unwrap());

    Ok(append_type(result, result_type))
}

The offchain coprocessor will pickup these computation request and perform the required computation offchain. By fetching relevant ciphertext corresponding to the handle/pointer, decrypting the ciphertext within TEE and performing the request computation on top of the plaintext and will encrypt the result the update the ciphertext against the resultant handle/pointer.