search

signalapp / libsignal

Home to the Signal Protocol as well as other cryptographic primitives which make Signal possible.
GNU Affero General Public License v3.0
3.63k stars 420 forks source link

Formal verification on the Rust code of Signal #510

Closed clarus closed 1 year ago

clarus commented 1 year ago

Hello,

How can we help apply formal verification techniques on the Rust code of Signal? What would be a good way to start / would that be of interest for Signal?

For now we are looking at the verification of the Subtle library from a kind suggestion of @cosmicexplorer , to check that all primitives execute in constant time. This is a training example of our project coq-of-rust to verify existing Rust code without modifications. Thanks.

Guillaume for Formal Land

jrose-signal commented 1 year ago

Hi! This isn't something we're directly interested in at this time, but feel free to discuss it with the community on the unofficial forums at https://community.signalusers.org/.

clarus commented 1 year ago

OK thanks! The link to the forum post: https://community.signalusers.org/t/formal-verification-on-the-code-of-signal/51490