Curious what the threat model for the cryptographic verification is. It looks like verify_signature_software[1] doesn't actually verify ed25519 signatures, but rather computes a truncated sha512 hash of the data and compares that with the supplied hash.
fn verify_signature_software(&self, data: &[u8], signature: &[u8; ED25519_SIGNATURE_LENGTH]) -> bool {
let mut h = [0u8; 64];
let data_hash = self.compute_sha512(data);
for i in 0..32 {
h[i] = data_hash[i];
}
self.verify_ed25519_reduced(h, signature)
}
This calls [1] which merely performs a byte equality check on the first 32 bytes of the hash:
fn verify_ed25519_reduced(&self, h: [u8; 64], signature: &[u8; ED25519_SIGNATURE_LENGTH]) -> bool {
// ...
let mut matches = true;
for i in 0..32 {
if signature[i] != h[i] {
matches = false;
break;
}
}
// ...
matches && key_valid
}
With this design, an adversary who knows data can simply calculate their own hash of the input data and supply it as a "signature", no?
It is difficult to comment on the verification approach when there are no secrets and only hash verification occurs. Do you have documentation on the approach and future plans? At best, this "signature verification" looks like placeholders for future verification.
Thank your question. The OS does have currently some limitations in the signature area, as this is one of those things that is still a work in progress due to trying to focus in many common threats first before expanding on the verification. It does perform hash comparisons, but then again, the proper ED25519 signature verification is still a work in progress.
The threat model is still evolving, but the core goal is to provide verifiable attestation of system operations with these key properties:
1. Non-repudiation of operations
2. Tamper-evidence for operation chains
3. Verifiable boot sequence attestation
You are absolutely right that the cryptographic aspects need significant hardening. I even have some key improvements planned for future versions:
1. Proper ED25519 signature implementation using the ring or ed25519-dalek crates
2. Secure key management for signing operation proofs
3. TPM integration for hardware-backed key storage and verification
4. Formal verification of the proof generation and verification logic
The core verification chain itself (in merkle_tree.rs and hash_chain.rs) provides tamper detection, but it does require significant hardening in the cryptographic area. Now being sincere, I really wanted to emphasize on the VKFS(verified kernel file system based on the Linux Ext2) implementation first as that was a very tough one to make.
Anyways, I really appreciate you diving into the code and highlighting this. ( * ´ ω ｀ * )
It is difficult to comment on the verification approach when there are no secrets and only hash verification occurs. Do you have documentation on the approach and future plans? At best, this "signature verification" looks like placeholders for future verification.
[0]: https://github.com/JGiraldo29/vekos/blob/d34e6454f3f7290e4b5...
[1]: https://github.com/JGiraldo29/vekos/blob/d34e6454f3f7290e4b5...