A verified messaging system

被引：15

作者：

Mansky W. ^{[1
]}

Appel A.W. ^{[1
]}

Nogin A. ^{[2
]}

机构：

[1] Department of Computer Science, Princeton University, Olden St., Princeton, 08544, NJ

[2] HRL Laboratories, LLC, 3011 Malibu Canyon Road, Malibu, 90265–4797, CA

来源：

Proceedings of the ACM on Programming Languages | 2017年 / 1卷 / OOPSLA期

基金：

美国国家科学基金会;

关键词：

Concurrent separation logic; Shared-memory communication; Shared-memory concurrency;

D O I：

10.1145/3133911

中图分类号：

学科分类号：

摘要：

We present a concurrent-read exclusive-write buffer system with strong correctness and security properties. Our motivating application for this system is the distribution of sensor values in a multicomponent vehicle-control system, where some components are unverified and possibly malicious, and other components are vehicle-control-critical and must be verified. Valid participants are guaranteed correct communication (i.e., the writer is always able to write to an unused buffer, and readers always read the most recently published value), while invalid readers or writers cannot compromise the correctness or liveness of valid participants. There is only one writer, all operations are wait-free, and there is no extra process or thread mediating communication. We prove the correctness of the system with valid participants by formally verifying a C implementation of the system in Coq, using the Verified Software Toolchain extended with an atomic exchange operation. The result is the first C-level mechanized verification of a nonblocking communication protocol. © 2017 Association for Computing Machinery.

引用

共 20 条

[1]

Appel A.W., Dockins R., Hobor A., Beringer L., Dodds J., Stewart G., Blazy S., Leroy X., Program Logics for Certified Compilers, (2014)

[2]

Blom S., Huisman M., Zaharieva-Stojanovski M., History-based verification of functional behaviour of concurrent programs, Proceedings of The 13th International Conference on Software Engineering and Formal Methods (SEFM 2015) (Lecture Notes in Computer Science), 9276, pp. 84-98, (2015)

[3]

Cofer D., Whalen M., Secure Mathematically-Assured Composition of Control Models (SMACCM), (2013)

[4]

Courtois P.J., Heymans F., Parnas D.L., Concurrent control with “Readers” and “Writers”, Commun. ACM, 14, 10, pp. 667-668, (1971)

[5]

Doko M., Vafeiadis V., Tackling real-life relaxed concurrency with FSL++, Proceedings of The 26th European Symposium on Programming (ESOP 2017) (Lecture Notes in Computer Science), pp. 448-475, (2017)

[6]

Hobor A., Appel A.W., Nardelli F.Z., Oracle semantics for concurrent separation logic, Proceedings of The 17th European Symposium on Programming (ESOP 2008) (Lecture Notes in Computer Science), 4960, pp. 353-367, (2008)

[7]

Holzmann G.J., Design and validation of protocols, Tutorial Computer Networks and ISDN Systems, 25, pp. 981-1017, (1990)

[8]

Jacobs B., Piessens F., Expressive modular fine-grained concurrency specification, Proceedings of The 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’11), pp. 271-282, (2011)

[9]

Jung R., Krebbers R., Birkedal L., Dreyer D., Higher-order ghost state, Proceedings of The 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), pp. 256-269, (2016)

[10]

Klein G., Elphinstone K., Heiser G., Andronick J., Cock D., Derrin P., Elkaduwe D., Engelhardt K., Kolanski R., Norrish M., Sewell T., Tuch H., Winwood S., SeL4: Formal verification of an OS kernel, Proceedings of The ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP ’09), pp. 207-220, (2009)

← 1 2 →