I have downloaded the slides from the site: [Compliance and Violation Patterns][1] It says No writes after calls. I can understand this concept. It’s a remedy for reentrancy problem. But it shows compliance and security patterns in some technical language related to Datalog or to some language related to software representation. Can some body please guide me what is the meaning of those equations?



They are statements about patterns of correct and incorrect code:

  1. For all call sites L1, there does not exist a store site L2 such that ... (and here I’m not clear—is that L2 may follow L1? Or that the truth of the statement may follow from the program, depending on L1 and L2?)
  2. For all call sites L1, there exists a store site L2 such that ... (idem.)
  • $\begingroup$ It would ofc be immensely helpful to provide details about the system in use here $\endgroup$ Nov 22 '19 at 16:45
  • 1
    $\begingroup$ Got it. Thanks a lot. God bless bless you. I also studied the "not" notation but I can't phrase the whole thing properly in English. "For all call sites L1, there does not exist a store site L2 such that L2 may follow L1", this seems correct. This is related to Securify tool in the context of reentrancy detection. Link of paper is: arxiv.org/pdf/1806.01143.pdf $\endgroup$ Nov 22 '19 at 17:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.