search

openwsn-berkeley / lakers

EDHOC implemented in Rust, optimized for microcontrollers, with bindings for C and Python.
https://crates.io/crates/lakers
BSD 3-Clause "New" or "Revised" License
13 stars 10 forks source link

Proper EC point validation #93

Open malishav opened 1 year ago

malishav commented 1 year ago

A PR on draft-ietf-lake-traces adds several invalid test vectors. Some of these contain messages with invalid G_X. In edhoc-rs, the point is not properly validated before the ECDH operation. This issue aims at adding point validation in process_message_1 and process_message_2 routines, which if failed, should return an error.

chrysn commented 10 months ago

When we do this, we may want to distinguish in the type system between "this is a buffer that holds a potential public key" and "this is a buffer that holds a valid public key".

chrysn commented 10 months ago

Proving freedom of panics (as I understand is one thing the hax converted thing can do) will be a tall order: It'll mean that the proof tool will need to remember that the only way to ever construct a public key is through the check at construction time, and that the branch that will later go from "this needs to be a valid point" to "otherwise I'll panic" will need to somehow match that knowledge.

Which, conversely, would allow incredibly defensive programming if the output of the proof could somehow be used on the Rust optimizer side to show that because there is proof of the property, the calculation doesn't have to be done again. Are there any plans to use that knowledge?