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

Memory-safety issues and information leakage are known to be depressinglycommon. We consider the compositional static detection of these kinds ofvulnerabilities in first-order C-like programs. Indeed the latter arerelational hyper-safety violations, comparing pairs of program executions,making them more challenging to detect than the former, which require reasoningonly over individual executions. Existing symbolic leakage detection methodstreat only non-interactive programs, avoiding the challenges of nondeterminism.Also, being whole-program analyses they cannot be appliedone-function-at-a-time, thereby ruling out incremental analysis. We remedythese shortcomings by presenting Insecurity Separation Logic (InsecSL), anunder-approximate relational program logic for soundly detecting informationleakage and memory-safety issues in interactive programs. Importantly, InsecSLreasons about pairs of executions, and so is relational, but purposefullyresembles the non-relational Incorrectness Separation Logic (ISL) that isalready automated in the Infer tool. We show how InsecSL can be automated bybi-abduction based symbolic execution, and we evaluate two implementations ofthis idea (one based on Infer) on various case-studies.

Compositional Vulnerability Detection with Insecurity Separation Logic (Extended Version)