search

makerdao / mkr-mcd-spec

High level KSpecification for the MCD System by Runtime Verification and Maker Foundation
GNU General Public License v3.0
28 stars 9 forks source link

Add flop blocking attack and property for detection #171

Closed kmbarry1 closed 4 years ago

kmbarry1 commented 4 years ago

Not really an attack, just gets the system into a state where flopping should happen but can't. If you change the heal call to a kiss call, you'll see that the second flop gets successfully kicked off.

kmbarry1 commented 4 years ago

Added a property to catch "blocked flop" situations. Sorry for kind of implementing it in a weird way (using binary digits of an Int for an Int to Bool mapping), but I couldn't get it to work using a Map (parsing errors).

Open to guidance on how to do this less weirdly, but at least this works.

kmbarry1 commented 4 years ago

(comments addressed)