3 ms·
That looks cool. Could you explain a bit more about how the formal verification part worked? What kind of prover do you use? Are the HSMs the specification, and
by oggy 12y ago
That looks cool. Could you explain a bit more about how the formal verification part worked? What kind of prover do you use? Are the HSMs the specification, and you want to make sure that the rules behave as specified by the HSMs, or do you specify some higher level properties on the HSMs? I couldn't figure these out scanning through your website.
- tlarkworthy 12y agoThe HSMs are converted to Firebase security rules. The theorem proover is used to verify somewhat arbitrary higher level properties So for item trade* I was specifying the that no new items could be introduced (dupe bugs) or removed from the system, and that a player could never get stuck in a state they could never leave (deadlock). The HSM abstraction is just a useful notation for developing such protocols, though the formal verification actually operated on the Firebase security rule level. * https://github.com/tomlarkworthy/firesafe/wiki/Send-Item https://github.com/tomlarkworthy/firesafe/wiki/Send-Item EDIT: reply to oggy's child question as I can't reply underneath. The actual spec prooving bit is secret sauce territory until I work out what the future holds for this project.
- oggy 12y agoThanks for the info. What theorem prover did you use and how do you convert the security rules to a format that the prover understands?