Per-Dereference Verification of Temporal Heap Safety via Adaptive Context-Sensitive Analysis

Yan, H; Chen, S; Sui, Y; Zhang, Y; Zou, C; Xue, J

Per-Dereference Verification of Temporal Heap Safety via Adaptive Context-Sensitive Analysis

Yan, H Chen, S Sui, Y

Zhang, Y Zou, C Xue, J

Permalink

Publication Type:: Conference Proceeding
Citation:: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2019, 11822 LNCS pp. 48 - 72
Issue Date:: 2019-01-01

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download Accepted manuscriptAdobe PDF (638.04 kB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Yan, H	en_US
dc.contributor.author	Chen, S	en_US
dc.contributor.author	Sui, Y https://orcid.org/0000-0002-9510-6574	en_US
dc.contributor.author	Zhang, Y	en_US
dc.contributor.author	Zou, C	en_US
dc.contributor.author	Xue, J	en_US
dc.date.issued	2019-01-01	en_US
dc.identifier.citation	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2019, 11822 LNCS pp. 48 - 72	en_US
dc.identifier.isbn	9783030323035	en_US
dc.identifier.issn	0302-9743	en_US
dc.identifier.uri	http://hdl.handle.net/10453/138549
dc.description.abstract	© Springer Nature Switzerland AG 2019. We address the problem of verifying the temporal safety of heap memory at each pointer dereference. Our whole-program analysis approach is undertaken from the perspective of pointer analysis, allowing us to leverage the advantages of and advances in pointer analysis to improve precision and scalability. A dereference (Forumala Presented)., say, via pointer q is unsafe iff there exists a deallocation (Forumala Presented)., say, via pointer p such that on a control-flow path (Forumala Presented).,p aliases with q (with both pointing to an object o representing an allocation), denoted, and (Forumala Presented). reaches (Forumala Presented). via control flow, denoted. Applying directly any existing pointer analysis, which is typically solved separately with an associated control-flow reachability analysis, will render such verification highly imprecise, since (i.e., (Forumala Presented). does not distribute over (Forumala Presented). ). For precision, we solve, with a control-flow path (Forumala Presented). containing an allocation o, a deallocation (Forumala Presented). and a dereference (Forumala Presented). abstracted by a tuple of three contexts. For scalability, a demand-driven full context-sensitive (modulo recursion) pointer analysis, which operates on pre-computed def-use chains with adaptive context-sensitivity, is used to infer, without losing soundness or precision. Our evaluation shows that our approach can successfully verify the safety of 81.3% (or (Forumala Presented).) of all the dereferences in a set of ten C programs totalling 1,166 KLOC.	en_US
dc.relation.ispartof	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)	en_US
dc.relation.isbasedon	10.1007/978-3-030-32304-2_4	en_US
dc.rights	info:eu-repo/semantics/openAccess
dc.subject.classification	Artificial Intelligence & Image Processing	en_US
dc.title	Per-Dereference Verification of Temporal Heap Safety via Adaptive Context-Sensitive Analysis	en_US
dc.type	Conference Proceeding
utslib.citation.volume	11822 LNCS	en_US
pubs.embargo.period	Not known	en_US
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology/School of Computer Science
pubs.organisational-group	/University of Technology Sydney/Strength - CAI - Centre for Artificial Intelligence
utslib.copyright.status	open_access	*
pubs.publication-status	Published	en_US
pubs.volume	11822 LNCS	en_US

Abstract:

© Springer Nature Switzerland AG 2019. We address the problem of verifying the temporal safety of heap memory at each pointer dereference. Our whole-program analysis approach is undertaken from the perspective of pointer analysis, allowing us to leverage the advantages of and advances in pointer analysis to improve precision and scalability. A dereference (Forumala Presented)., say, via pointer q is unsafe iff there exists a deallocation (Forumala Presented)., say, via pointer p such that on a control-flow path (Forumala Presented).,p aliases with q (with both pointing to an object o representing an allocation), denoted, and (Forumala Presented). reaches (Forumala Presented). via control flow, denoted. Applying directly any existing pointer analysis, which is typically solved separately with an associated control-flow reachability analysis, will render such verification highly imprecise, since (i.e., (Forumala Presented). does not distribute over (Forumala Presented). ). For precision, we solve, with a control-flow path (Forumala Presented). containing an allocation o, a deallocation (Forumala Presented). and a dereference (Forumala Presented). abstracted by a tuple of three contexts. For scalability, a demand-driven full context-sensitive (modulo recursion) pointer analysis, which operates on pre-computed def-use chains with adaptive context-sensitivity, is used to infer, without losing soundness or precision. Our evaluation shows that our approach can successfully verify the safety of 81.3% (or (Forumala Presented).) of all the dereferences in a set of ten C programs totalling 1,166 KLOC.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/138549