3 ms·

I wrote a state machine abstraction for Firebase [1], then implemented cross tree transactions on top, which was the formally verified to be exploit free. I thi

I wrote a state machine abstraction for Firebase [1], then implemented cross tree transactions on top, which was the formally verified to be exploit free. I think co-routines are a bit too general to make formal verification straight forward. [1] http://tomlarkworthy.github.io/ http://tomlarkworthy.github.io/

erichocean 13y ago
That is a seriously cool project! I wish more people took advantage of both HSMs and theorem provers, and you've done both. Nice. :)
- tlarkworthy 13y ago
  thanks a lot. Yeah, its a brutal bug exterminator combo, and somewhat easier to wrap your head around that coq or similar. I am trying to find an organic use of the H in HSM for server side stuff, but struggling to think of examples that are not contrived if you have any.
oggy 13y 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 13y ago
  The 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 13y ago
    Thanks for the info. What theorem prover did you use and how do you convert the security rules to a format that the prover understands?

erichocean 13y ago

That is a seriously cool project! I wish more people took advantage of both HSMs and theorem provers, and you've done both. Nice. :)

tlarkworthy 13y ago
thanks a lot. Yeah, its a brutal bug exterminator combo, and somewhat easier to wrap your head around that coq or similar. I am trying to find an organic use of the H in HSM for server side stuff, but struggling to think of examples that are not contrived if you have any.

oggy 13y 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 13y ago
The 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 13y ago
  Thanks for the info. What theorem prover did you use and how do you convert the security rules to a format that the prover understands?