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.