Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Issue title: Selected papers from the 35th IEEE Computer Security Foundations Symposium – CSF 2022
Guest editors: Stefano Calzavara and David Naumann
Article type: Research Article
Authors: Li, Liyia; * | Liu, Yiyunb | Postol, Deenaa | Lampropoulos, Leonidasa | Van Horn, Davida | Hicks, Michaela; c; **
Affiliations: [a] Department of Computer Science, University of Maryland, College Park, MD, USA | [b] Department of Computer and Information Science, University of Pennsylvania, PA, USA | [c] Amazon, VA, USA
Correspondence: [*] Corresponding author. E-mail: liyili2@umd.edu.
Note: [1] This paper is an extended and revised version of a paper presented at CSF’22.
Note: [**] Michael Hicks’ work was completed prior to starting at Amazon.
Abstract: We present a formal model of Checked C, a dialect of C that aims to enforce spatial memory safety. Our model pays particular attention to the semantics of dynamically sized, potentially null-terminated arrays. We formalize this model in Coq, and prove that any spatial memory safety errors can be blamed on portions of the program labeled unchecked; this is a Checked C feature that supports incremental porting and backward compatibility. While our model’s operational semantics uses annotated (“fat”) pointers to enforce spatial safety, we show that such annotations can be safely erased. Using PLT Redex we formalize an executable version of our model and a compilation procedure to an untyped C-like language, as well as use randomized testing to validate that generated code faithfully simulates the original. Finally, we develop a custom random generator for well-typed and almost-well-typed terms in our Redex model, and use it to search for inconsistencies between our model and the Clang Checked C implementation. We find these steps to be a useful way to co-develop a language (Checked C is still in development) and a core model of it.
Keywords: C, Checked C, spatial safety, compiler verification
DOI: 10.3233/JCS-230040
Journal: Journal of Computer Security, vol. 31, no. 5, pp. 581-614, 2023
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl