Arseniy Zaostrovnykh
Luis Pedrosa
George Candea
ABSTRACT
We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of network functions and proves properties specific to network configuration, such as reachability and absence of loops. Our proof applies directly to the C code of a network function, and it demonstrates the absence of implementation bugs. Prior work argued that this is not feasible (i.e., that verifying a real, stateful network function written in C does not scale) but we demonstrate otherwise: NAT is one of the most popular network functions and maintains per-flow state that needs to be properly updated and expired, which is a typical source of verification challenges. We tackle the scalability challenge with a new combination of symbolic execution and proof checking using separation logic; this combination matches well the typical structure of a network function. We then demonstrate that formally proven correctness in this case does not come at the cost of performance. The NAT code, proof toolchain, and proofs are available at [58].
Supplemental Material
- Barnett, M., Chang, B.-Y. E., DeLine, R., Jacobs, B., and Leino, K. R. M. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects (2005).Google Scholar
- Beringer, L., Petcher, A., Katherine, Q. Y., and Appel, A. W. Verified Correctness and Security of OpenSSL HMAC. In USENIX Security Symp. (2015).Google Scholar
- Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., and Wansbrough, K. Rigorous Specification and Conformance Testing Techniques for Network Protocols, as applied to TCP, UDP, and Sockets. SIGCOMM Computer Communication Review 35, 4 (2005). Google ScholarDigital Library
- Blanchette, J., Bulwahn, L., and Nipkow, T. Automatic Proof and Disproof in Isabelle/HOL. Frontiers of Combining Systems (2011).Google Scholar
- Boye, M. Netfilter Connection Tracking and NAT Implementation. In Seminar on Network Protocols in Operating Systems (2013).Google Scholar
- Boyer, R. S., Elspas, B., and Levitt, K. N. SELECT -- A Formal System for Testing and Debugging Programs by Symbolic Execution. SIGPLAN Notices 10 (1975). Google ScholarDigital Library
- Bradner, S., and McQaid, J. Benchmarking Methodology for Network Interconnect Devices. RFC 2544, RFC Editor, 1999.Google Scholar
- Brocade Vyatta Network OS. http://www.brocade.com/en/products-services/software-networking/network-functions-virtualization/vyatta-network-os.html. Accessed: 2017-01-24.Google Scholar
- Cadar, C., Dunbar, D., Engler, D. R., et al. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Symp. on Operating Sys. Design and Implem. (2008).Google ScholarDigital Library
- Canini, M., Venzano, D., Perešíni, P., Kostić, D., and Rexford, J. A NICE Way to Test OpenFlow Applications. In Symp. on Networked Systems Design and Implem. (2012).Google ScholarDigital Library
- Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M. F., and Zeldovich, N. Using Crash Hoare Logic for Certifying the FSCQ File System. In Symp. on Operating Systems Principles (2015). Google ScholarDigital Library
- Chlipala, A. Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic. SIGPLAN Notices 46, 6 (2011). Google ScholarDigital Library
- Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. Counterexample-Guided Abstraction Refinement. In Intl. Conf. on Computer Aided Verification (2000). Google ScholarCross Ref
- Clarke, L. A. A Program Testing System. In Annual ACM Conf. (1976). Google ScholarDigital Library
- CVE-2013-1138. Available from CVE Details, CVE-ID CVE-2013-1138., 2013.Google Scholar
- CVE-2014-3817. Available from CVE Details, CVE-ID CVE-2014-3817., 2014.Google Scholar
- CVE-2015-6271. Available from CVE Details, CVE-ID CVE-2015-6271., 2015.Google Scholar
- CVE-2014-9715. Available from CVE Details, CVE-ID CVE-2014-9715., 2014.Google Scholar
- Dobrescu, M., and Argyraki, K. Software Dataplane Verification. In Symp. on Networked Systems Design and Implem. (2014).Google ScholarDigital Library
- Dobrescu, M., Egi, N., Argyraki, K., Chun, B.-G., Fall, K., Iannaccone, G., Knies, A., Manesh, M., and Ratnasamy, S. RouteBricks: Exploiting Parallelism To Scale Software Routers. In Symp. on Operating Systems Principles (2009).Google ScholarDigital Library
- Data Plane Development Kit. http://dpdk.org. Accessed: 2017-06-16.Google Scholar
- Emmerich, P., Gallenmüller, S., Raumer, D., Wohlfart, F., and Carle, G. MoonGen: A Scriptable High-Speed Packet Generator. In Internet Measurement Conference (2015). Google ScholarDigital Library
- Ernst, M. D., Cockrell, J., Griswold, W. G., and Notkin, D. Dynamically Discovering Likely Program Invariants to Support Program Evolution. IEEE Transactions on Software Engineering 27, 2 (2001). Google ScholarDigital Library
- Fayaz, S. K., Yu, T., Tobioka, Y., Chaki, S., and Sekar, V. BUZZ: Testing Context-Dependent Policies in Stateful Networks. In Symp. on Networked Systems Design and Implem. (2016).Google Scholar
- Fogel, A., Fung, S., Pedrosa, L., Walraed-Sullivan, M., Govindan, R., Mahajan, R., and Millstein, T. A General Approach to Network Configuration Analysis. In Symp. on Networked Systems Design and Implem. (2015).Google Scholar
- Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J. R., Parno, B., Roberts, M. L., Setty, S., and Zill, B. IronFleet: Proving Practical Distributed Systems Correct. In Symp. on Operating Systems Principles (2015).Google ScholarDigital Library
- Howden, W. Symbolic Testing and the DISSECT Symbolic Evaluation System. IEEE Transactions on Software Engineering 3, 4 (1977). Google ScholarDigital Library
- Jacobs, B., and Piessens, F. The VeriFast Program Verifier. Tech. Rep. CW-520, Department of Computer Science, KU Leuven, 2008.Google Scholar
- Kadlecsik, J., and Pásztor, G. Netfilter Performance Testing. Tech. rep., Netfilter Project, Berlin, Germany, 2004.Google Scholar
- Kazemian, P., Chan, M., Zeng, H., Varghese, G., McKeown, N., and Whyte, S. Real Time Network Policy Checking Using Header Space Analysis. In Symp. on Networked Systems Design and Implem. (2013).Google Scholar
- Kazemian, P., Varghese, G., and McKeown, N. Header Space Analysis: Static Checking For Networks. In Symp. on Networked Systems Design and Implem. (2012).Google Scholar
- Khurshid, A., Zou, X., Zhou, W., Caesar, M., and Godfrey, P. B. VeriFlow: Verifying Network-Wide Invariants in Real Time. In Symp. on Networked Systems Design and Implem. (2013).Google Scholar
- King, J. C. Symbolic Execution and Program Testing. J. ACM 19, 7 (1976). Google ScholarDigital Library
- Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al. seL4: Formal Verification of an OS Kernel. In Symp. on Operating Systems Principles (2009).Google Scholar
- Kohler, E., Morris, R., Chen, B., Jannotti, J., and Kaashoek, M. F. The Click Modular Router. ACM Transactions on Computer Systems 18, 3 (2000). Google ScholarDigital Library
- Kuzniar, M., Peresini, P., Canini, M., Venzano, D., and Kostic, D. A SOFT Way for OpenFlow Switch Interoperability Testing. In Proceedings of the 8th international conference on Emerging networking experiments and technologies (2012). Google ScholarDigital Library
- Lee, B.-S., and Bryant, B. R. Automated Conversion from Requirements Documentation to an Object-oriented Formal Specification Language. In Symposium on Applied Computing (2002). Google ScholarDigital Library
- Lopes, N. P., Bjørner, N., Godefroid, P., Jayaraman, K., and Varghese, G. Checking Beliefs in Dynamic Networks. In Symp. on Networked Systems Design and Implem. (2015).Google Scholar
- Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, P. B., and King, S. T. Debugging the Data Plane with Anteater. In ACM SIGCOMM Conf. (2011). Google ScholarDigital Library
- MS13-064. Available from CVE Details, CVE-ID MS13-064., 2013.Google Scholar
- Musuvathi, M., Engler, D. R., et al. Model Checking Large Network Protocol Implementations. In Symp. on Networked Systems Design and Implem. (2004), vol. 4.Google Scholar
- Nagarakatte, S., Zhao, J., Martin, M. M., and Zdancewic, S. SoftBound: Highly Compatible and Complete Spatial Memory Safety for C. SIGPLAN Notices 44, 6 (2009). Google ScholarDigital Library
- Nagarakatte, S., Zhao, J., Martin, M. M., and Zdancewic, S. CETS: Compiler Enforced Temporal Safety for C. SIGPLAN Notices 45, 8 (2010). Google ScholarDigital Library
- O'Hearn, P. W., Reynolds, J. C., and Yang, H. Local Reasoning about Programs that Alter Data Structures. In CSL (2001). Google ScholarCross Ref
- Padhi, S., Sharma, R., and Millstein, T. Data-Driven Precondition Inference with Learned Features. In Intl. Conf. on Programming Language Design and Implem. (2016). Google ScholarDigital Library
- Panda, A., Lahav, O., Argyraki, K., Sagiv, M., and Shenker, S. Verifying Reachability in Networks with Mutable Datapaths. In Symp. on Networked Systems Design and Implem. (2017).Google Scholar
- Perkins, J. H., and Ernst, M. D. Efficient Incremental Algorithms for Dynamic Detection of Likely Invariants. ACM SIGSOFT Software Engineering Notes 29, 6 (2004). Google ScholarDigital Library
- Postel, J. Discard Protocol. RFC 863, RFC Editor, 1983.Google Scholar
- Primorac, M., Argyraki, K., and Bugnion, E. How to Measure the Killer Microsecond. In ACM SIGCOMM Workshop on Kernel-Bypass Networks (2017). Google ScholarDigital Library
- Ramamoorthy, C., Ho, S.-B., and Chen, W. On the Automated Generation of Program Test Data. IEEE Transactions on Software Engineering 2, 4 (1976). Google ScholarDigital Library
- Reynolds, J. C. Separation Logic: A Logic for Shared Mutable Data Structures. In IEEE-LCS (2002). Google ScholarCross Ref
- Ryzhyk, L., Bjørner, N., Canini, M., Jeannin, J.-B., Schlesinger, C., Terry, D. B., and Varghese, G. Correct by Construction Networks Using Stepwise Refinement. In Symp. on Networked Systems Design and Implem. (2017).Google Scholar
- Srisuresh, P., and Egevang, K. Traditional IP Network Address Translator (Traditional NAT). RFC 3022, RFC Editor, 2001.Google Scholar
- Stewart, G., Beringer, L., Cuellar, S., and Appel, A. W. Compositional CompCert. SIGPLAN Notices 50, 1 (2015). Google ScholarDigital Library
- Stoenescu, R., Popovici, M., Negreanu, L., and Raiciu, C. SymNet: scalable symbolic execution for modern networks. In ACM SIGCOMM Conf. (2016). Google ScholarDigital Library
- Tange, O. GNU Parallel - The Command-Line Power Tool.; login: The USENIX Magazine 36, 1 (2011).Google Scholar
- Clang 5 documentation - UndefinedBehaviorSanitizer - Available checks. https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html#available-checks. Accessed: 2017-01-24.Google Scholar
- VigNAT Project Repository. https://vignat.github.io, 2017.Google Scholar
- Xie, G. G., Zhan, J., Maltz, D. A., Zhang, H., Greenberg, A., Hjalmtysson, G., and Rexford, J. On Static Reachability Analysis of IP Networks. In Intl. Conf. on Computer Communications (INFOCOM) (2005). Google ScholarCross Ref
- Zaostrovnykh, A., Argyraki, K., and Candea, G. Nework software verification survey. https://vignat.github.io/survey, Feb. 2016.Google Scholar
Index Terms
- A Formally Verified NAT
Recommendations
A formally verified NAT stack
Prior work proved a stateful NAT network function to be, crash-free, memory safe and semantically correct [29]. Their toolchain verifies the network function code while assuming the underlying kernel-bypass framework, drivers, operating system, and ...
A Formally Verified NAT Stack
KBNets'18: Proceedings of the 2018 Afternoon Workshop on Kernel Bypassing NetworksPrior work proved a stateful NAT network function to be semantically correct, crash-free, and memory safe [29]. Their toolchain verifies the network function code while assuming the underlying kernel-bypass framework, drivers, operating system, and ...
Verifying verified code
AbstractA recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow-up case study that explores the methodology from the perspective of three research ...
Comments