lnu.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Symbolic Abstract Heaps for Polymorphic Information-Flow Guard Inference
University of Liverpool, UK.
Linnaeus University, Faculty of Technology, Department of computer science and media technology (CM). Newcastle University, UK.ORCID iD: 0000-0002-0377-5595
2023 (English)In: Verification, Model Checking, and Abstract Interpretation. VMCAI 2023. / [ed] Dragoi, C., Emmi, M., Wang, J., Springer, 2023, Vol. 13881 LNCS, p. 66-90Conference paper, Published paper (Refereed)
Abstract [en]

In the realm of sound object-oriented program analyses for information-flow control, very few approaches adopt flow-sensitive abstractions of the heap that enable a precise modeling of implicit flows. To tackle this challenge, we advance a new symbolic abstraction approach for modeling the heap in Java-like programs. We use a store-less representation that is parameterized with a family of relations among references to offer various levels of precision based on user preferences. This enables us to automatically infer polymorphic information-flow guards for methods via a co-reachability analysis of a symbolic finite-state system. We instantiate the heap abstraction with three different families of relations. We prove the soundness of our approach and compare the precision and scalability obtained with each instantiated heap domain by using the IFSpec benchmarks and real-life applications.

Place, publisher, year, edition, pages
Springer, 2023. Vol. 13881 LNCS, p. 66-90
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 13881
Keywords [en]
Abstracting, Computer software, Object oriented programming, Flow sensitive, Information flow control, Information flows, Java-like programs, Object-oriented program, Parameterized, Precise modeling, Program analysis, Reachability analysis, User’s preferences, Benchmarking
National Category
Computer Sciences
Research subject
Computer and Information Sciences Computer Science, Computer Science
Identifiers
URN: urn:nbn:se:lnu:diva-123724DOI: 10.1007/978-3-031-24950-1_4Scopus ID: 2-s2.0-85148694768ISBN: 9783031249495 (print)ISBN: 9783031249501 (electronic)OAI: oai:DiVA.org:lnu-123724DiVA, id: diva2:1788103
Conference
24th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2023; Conference date: 16 January 2023 through 17 January 2023;
Available from: 2023-08-15 Created: 2023-08-15 Last updated: 2023-09-07Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Khakpour, Narges

Search in DiVA

By author/editor
Khakpour, Narges
By organisation
Department of computer science and media technology (CM)
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 33 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf