English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Methods for proving that concurrent software does not leak its secrets hasremained an active topic of research for at least the past four decades.Despite an impressive array of work, the present situation remains highlyunsatisfactory. With contemporary compositional proof methods one is forced tochoose between expressiveness (the ability to reason about a wide variety ofsecurity policies), on the one hand, and precision (the ability to reason aboutcomplex thread interactions and program behaviours), on the other. Achievingboth is essential and, we argue, requires a new style of compositionalreasoning.  We present VERONICA, the first program logic for proving concurrent programsinformation flow secure that supports compositional, high-precision reasoningabout a wide range of security policies and program behaviours (e.g. expressivede-classification, value-dependent classification, secret-dependent branching).Just as importantly, VERONICA embodies a new approach for engineering suchlogics that can be re-used elsewhere, called decoupled functional correctness(DFC). DFC leads to a simple and clean logic, even while achieving thisunprecedented combination of features. We demonstrate the virtues andversatility of VERONICA by verifying a range of example programs, beyond thereach of prior methods.

VERONICA: Expressive and Precise Concurrent Information Flow Security (Extended Version with Technical Appendices)