Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks

【Author】 Albert, Elvira; Grossman, Shelly; Rinetzky, Noam; Rodriguez-Nunez, Clara; Rubio, Albert; Sagiv, Mooly

【Source】IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING

【影响因子】6.791

【Abstract】Callbacks are an essential mechanism for event-driven programming. Unfortunately, callbacks make reasoning challenging because they introduce behaviors where calls to the module are interleaved. We present a parametric method that, from a particular invariant of the program, allows reducing the problem of verifying the invariant in the presence of callbacks, to the callback-free setting. Intuitively, we allow callbacks to introduce behaviors that cannot be produced by callback free executions, as long as they do not affect correctness. A chief insight is that the user is aware of the potential effect of the callbacks on the program state. To this end, we present a parametric verification technique which accepts this insight as a relation between callback and callback free executions. We implemented our approach and applied it successfully to a large set of real-world programs.

【Keywords】Contracts; Cognition; Codes; Programming; Static analysis; Smart contracts; Safety; Smart contract verification; Event-driven programming; Unbounded re-entrancy; Callbacks

【发表时间】2023 MAY-JUN

【收录时间】2023-07-04

【文献类型】

【主题类别】

--