scaspin/memory-safe-assembly

Bottom-up memory-safety for assembly language using symbolic execution

memory-safe-assembly's Issues

Support SIMD Instructions in Symbolic Execution

Required sub-tasks:

• New register type
• Model overlapping registers (e.g. operations on vector registers should affect non-vector versions of underlying registers, etc) unnecessary: focus on Neon first which is a separate register file, specification here.
• Interpret vector instructions
• Export & validate gcm_init_neon

Support AES hardware instructions for AARCH64

TODO: figure out what needs to be done for this. Reflect in issue description (here!) like in #16

Copy all relevant AARCH64 Linux and iOS generated assembly files from generated srcs in aws-lc & port to compile in BUMS repo

Add wrappers to unvalidable assembly procedures in boringSSL that will validate

At least:

• SHA256
• AES CTR 128

Build infrastructure to cross compile and run Linux-AARCH64 AWS LC examples on Linux x86_64

Support miscellaneous remaining AARCH64 instructions used in boringSSL

• movz
• movk
• (fill in as we find more...)

Implement `AES_ctr128_encrypt` from aws-lc in Rust against validated assembly for aarch64 Linux & iOS

Match this signature exactly: https://docs.rs/aws-lc-sys/latest/aws_lc_sys/fn.AES_ctr128_encrypt.html