0
$\begingroup$

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?

Zulfi.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

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.)
Improve this answer
$\endgroup$
2
  • $\begingroup$ It would ofc be immensely helpful to provide details about the system in use here $\endgroup$
    – D. Ben Knoble
    Commented Nov 22, 2019 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$
    – user2994783
    Commented Nov 22, 2019 at 17:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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