×

Proving the correctness of client/server software. (English) Zbl 1177.68045

Summary: Remote Procedure Calls (RPCs) lie at the heart of any client/server software. Thus, formal specification and verification of RPC mechanisms is a prerequisite for the verification of any such software. In this paper, we present a mathematical specification of an RPC mechanism and we outline how to prove the correctness of an implementation – say written in C – of this mechanism at the code level. We define a formal model of user processes running concurrently under a simple operating system, which provides inter-process communication and portmapper system calls. A simple theory of non-interference permits us to use conventional sequential program analysis between system calls (within the concurrent model). An RPC mechanism is specified and the correctness proof for server implementations, using this mechanism, is outlined. To the best of our knowledge this is the first treatment of the correctness of an entire RPC mechanism at the code level.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

veriSoft
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Alkassar E, Böhm P, Knapp S 2008a Formal correctness of a gate-level automotive bus controller implementation. In B Kleinjohann, L Kleinjohann, W Wolf, eds., 6th IFIP Working Conference on Distributed and Parallel Embedded Systems (DIPES08), 57–68. Springer
[2] Alkassar E, Schirmer N, Starostin A 2008b Formal pervasive verification of a paging mechanism. In CR Ramakrishnan, J Rehof, eds., 14th intl Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS08), volume 4963 of LNCS, 109–123. Springer · Zbl 1134.68394
[3] Arkoudas K, Zee K, Kuncak V, Rinard M 2004 Verifying a file system implementation. In Sixth International Conference on Formal Engineering Methods, volume 3308 of LNCS 373–390
[4] Beckert B, Beuster G 2004 Formal specification of security-relevant properties of user interfaces. In Proceedings, 3rd International Workshop on Critical Systems Development with UML, Lisbon, Portugal, Munich, Germany. TU Munich Technical Report TUM-I0415
[5] Beuster G, Bormer T, Markus Wagner P B 2007 Code-level verification of an email client. http://www.verisoft.de/.rsrc/VerisoftRepository/vemail-trunk-r15868.tar.gz
[6] Beuster G, Henrich N, Wagner M 2006 Real world verification–experiences from the Verisoft email client. In Proceedings of the Workshop on Empirical Succesfully Computerized Reasoning (ESCoR 2006)
[7] Bevier W R 1989 Kit and the short stack. Journal of Automated Reasoning, 5(4): 519–530
[8] Bevier W R, Cohen R 1996 An executable model of the Synergy file system. Technical Report 121, Computational Logic Inc
[9] Bevier W R, Hunt Jr. WA, Moore J S, Young WD 1989 An approach to systems verification. Journal of Automated Reasoning 5(4): 411–428. ISSN 0168-7433
[10] Beyer S 2005 Putting it all together - Formal Verification of the VAMP. PhD thesis, Saarland University, Saarbrücken
[11] Beyer S, Jacobi C, Kröning D, Leinenbach D C, Paul W J 2005 Putting it all together – formal verification of the VAMP. International Journal on Software Tools for Technology Transfer
[12] Birrell A D, Nelson B J 1984 Implementing remote procedure calls. ACM Trans. Comput. Syst. 2(1): 39–59. ISSN 0734-2071 · doi:10.1145/2080.357392
[13] Bishop S, Fairbairn M, Norrish M, Sewell P, Smith M, Wansbrough K 2005 TCP, UDP, and sockets: Rigorous and experimentally-validated behavioural specification: Volume 3: Overview. Technical report, University of Cambridge
[14] Bogan S 2007 Academic System–Demo 2007 Talk given at the 3rd German Verification Day. http://www-wjp.cs.uni-sb.de/leute/private_homepages/sebastian/Demo2.mov
[15] Bogan S 2008a Formal Specification of a Simple Operating System. PhD thesis, Saarland University, Saarbrücken
[16] Bogan S 2008b Isabelle/HOL specification of the SOS. http://www.verisoft.de/.rsrc/VerisoftRepository/sos-trunk-r22974.tar.gz
[17] Bormann J, Beyer S, Maggiore A, Blackmore T 2007 Complete formal verification of tricore2 and other processors. In Design and Verification conference (DVCon 2007)
[18] Broy M, Merz S, Spies K 1996 The rpc-memory case study: A synopsis. In Formal Systems Specification, The RPC-Memory Specification Case Study (the book grow out of a Dagstuhl Seminar, September 1994), pages 5–20, London, UK. Springer-Verlag. ISBN 3-540-61984-4
[19] Cohen E 2000 Separation and reduction. In MPC’00, pages 45–59. Springer. ISBN 3-540-67727-5 · Zbl 0963.68504
[20] Cohen E, Lamport L 1998 Reduction in TLA. In CONCUR’98, pages 317–331, London, UK. Springer. ISBN 3-540-64896-8
[21] Dalinger I 2006 Formal Verification of a Processor with Memory Management Units. PhD thesis, Saarland University
[22] Daum M 2008 Modelling user programs on top of a microkernel. In Troubitsyna E, editor, Proceedings of Doctoral Symposium held in conjunction with Formal Methods 2008, volume 48 of General Publications. Turku centre for computer science. http://www-wjp.cs.unisb.de/publikationen/Daum_FM08ds-.pdf
[23] Dörrenbächer J 2006 VAMOS microkernel: Formal models and verification 2006 Talk given at the International Workshop on Systems Software Verification, Australia, August 7–8, 2006. http://www.cse.unsw.edu.au/formalmethods/events/svws-06/VAMOS-Microker nel.pdf
[24] Elphinstone K, Klein G, Derrin P, Roscoe T, Heiser G 2007 Towards a practical, verified kernel. In 11th Workshop on Hot Topics in Operating Systems, page 6, San Diego, CA, USA
[25] Grünbacher A 2003 POSIX Access Control Lists on Linux. In USENIX Annual Technical Conference, FREENIX Track 259–272
[26] Härtig H, Hohmuth M, Feske N, Helmuth C, Lackorzynski A, Mehnert F, Peter M 2005 The Nizza secure-system architecture. In Proceedings of the 1st International Conference on Collaborative Computing: Networking, Applications and Worksharing
[27] Hillebrand M A, Paul W J 2007 On the architecture of system verification environments. In Haifa Verification Conference 2007, October 23–25, 2007, Haifa, Israel, LNCS. Springer
[28] Hohmuth M, Tews H 2005 The VFiasco approach for a verified operating system. In 2nd ECOOP Workshop on Programm Languages and Operating Systems
[29] IEEE 2004 IEEE std. 1003 {\(\cdot\)} 1, 2004 edition. The Open Group Technical Standard. Base specifications, issue 6. Includes IEEE std 1003 {\(\cdot\)} 1-2001, IEEE std 1003 {\(\cdot\)} 1-2001/cor 1-2002 and IEEE std 100 {\(\cdot\)} 1-2001/cor 2-2004. Shell and utilities, 2004
[30] Jacobi C, Weber K, Paruthi V, Baumgartner J 2005 Automatic formal verification of fused-multiplyadd fpus. In DATE’ 05: Proceedings of the conference on Design, Automation and Test in Europe, pages 1298–1303, Washington, DC, USA. IEEE Computer Society. ISBN 0-7695-2288-2
[31] Joshi R, Holzmann G J 2007 A mini challenge: Build a verifiable filesystem. Formal Aspects of Computing 19(2): 269–272 · Zbl 1123.68336 · doi:10.1007/s00165-006-0022-3
[32] Knapp S, Paul W J 2007 Realistic Worst Case Execution Time Analysis in the Context of Pervasive System Verification. In Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm, volume 4444 of LNCS · Zbl 1149.68405
[33] Lamport L, Melliar-Smith P M 1985 Synchronizing clocks in the presence of faults. J. ACM 32(1): 52–78. ISSN 0004-5411 · Zbl 0629.68025 · doi:10.1145/2455.2457
[34] Langenstein B, Nonnengart A, Rock G, Stephan W 2007a A history-based verification of distributed applications. In Beckert B, editor, Proceedings, 4th International Verification Workshop (VERIFY), Bremen, Germany. CEUR-WS Workshop Proceedings · Zbl 1098.68545
[35] Langenstein B, Nonnengart A, Rock G, Stephan W 2007b Verification of distributed applications. In F Saglietti, N Oster, eds., Computer Safety, Reliability, and Security, 26th International Conference, SAFECOMP 2007, Nuremberg, Germany, September 18–21, 2007, volume 4680 of LNCS 315–328. Springer
[36] Leinenbach D C 2008 Compiler Verification in the Context of Pervasive System Verification. PhD thesis, Saarland University, Saarbrücken
[37] Leinenbach D C, Paul W J, Petrova E 2005a Towards the formal verification of a C0 compiler: Code generation and implementation correctness. In Aichernig B and Beckert B, editors, 3rd International Conference on Software Engineering and Formal Methods (SEFM 2005), 5–9 September 2005, Koblenz, Germany 2–11
[38] Leinenbach D C, Paul W J, Petrova E 2005b Towards the formal verification of a C0 compiler: Code generation and implementation correctness. In 3rd International Conference on Software Engineering and Formal Methods, 5–9 September 2005, Koblenz, Germany
[39] Leinenbach DC, Petrova E 2008 Pervasive compiler verification–From verified programs to verified systems. In 3rd International Workshop on Systems Software Verification
[40] Lipton R J 1975 Reduction: A method of proving properties of parallel programs. Commun. ACM 18(12): 717–721. ISSN 0001-0782 · Zbl 0316.68015 · doi:10.1145/361227.361234
[41] Lynch N A 1996 Distributed Algorithms. Morgan Kaufmann 1996 ISBN 1-55860-348-4
[42] Moore J S, Lynch T, Kaufmann M 1998 A mechanically checked proof of the amd5k86 floating point devision program. In 10th Anniversary Colloquium of UNU/IIST, volume 47(9). IEEE Transactions on Computers · Zbl 1392.68051
[43] Moore J S 2003 A grand challenge proposal for formal methods: A verified stack. In B K Aichernig, T S E Maibaum, eds., 10th Anniversary Colloquium of UNU/IIST, volume 2757 of LNCS, pages 161–172. Springer. ISBN 3-540-20527-6
[44] OSEK/VDX time-triggered operating system. OSEK group 2001. http://www.osek-vdx.org/mirror/ttos10.pdf
[45] Peled D 1998 Ten years of partial order reduction. In CAV’ 98: Proceedings of the 10th International Conference on Computer Aided Verification, pages 17–28, London, UK. Springer-Verlag. ISBN 3-540-64608-6
[46] Petrova E 2007 Verification of the C0 Compiler Implementation on the Source Code Level. PhD thesis, Saarland University, Saarbrücken
[47] Pfitzmann B, Riordan J, Stüble C, Waidner M, Weber A 2001 The PERSEUS system architecture. In D Fox, M Köhntopp, A Pfitzmann, eds., VIS 2001, Sicherheit in komplexen IT-Infrastrukturen, pages 1–18. Vieweg
[48] Rieden T I d, Tsyban A 2008 Cvm – a verified framework for microkernel programmers. In 3rd intl Workshop on Systems Software Verification (SSV08). Elsevier Science B.V
[49] Rieden T 2008 CVM–A Formally Verified Framework for Microkernel Programmers. PhD thesis, Saarland University, Saarbrücken. to appear
[50] Rieden T, Tsyban A 2008 CVM – A verified framework for microkernel programmers. In 3rd International Workshop on Systems Software Verification
[51] Sawada J, Hunt WA 1998 Processor Verification with Precise Exceptions and Speculative Execution. In A J Hu, M Y Vardi, eds., CAV’98 135–146. Springer. ISBN 3-540-64608-6
[52] Schirmer N W 2005 Verification of Sequential Imperative Programs in Isabelle/HOL. PhD thesis, Technical University of Munich · Zbl 1108.68410
[53] Schmaltz J 2006 A Formal Model of Lower System Layers. In FMCAD’06, pages 191–192, Los Alamitos, CA, USA. IEEE Computer Society. ISBN 0-7695-2707-8
[54] Shadrin A 2006 Design and implementation of the portmapper and RPC primitives in the context of the SOS. Master’s thesis, Saarland University, Saarbrücken
[55] Shapiro J S, Doerrie MS, Northup E, Sridhar S, Miller MS 2004 Towards a verified, general-purpose operating system kernel. In G Klein, ed., Proc. NICTA FM Workshop on OS Verification. Technical Report 0401005T-1, pages 1–19. National ICT Australia
[56] Shepler S, Callaghan B, Robinson D, Thurlow R, Beame C, Eisler M, Noveck D, 2003. RFC 3530: Network file system (nfs) version 4 protocol, 2003
[57] Sikkel K, Stiemerling O 1998 User-oriented authorization in collaborative environments, 1998
[58] Smith M A 1996 Formal Verification of TCP and T/TCP. PhD thesis, Massachusetts Institute of Technology
[59] Srinivasan R 1995 RFC 1831: RPC: Remote procedure call protocol specification version 2 1995. ftp://ftp.internic.net/rfc/rfc1831.txt
[60] Starostin A 2006 Formal verification of a c-library for strings. Master’s thesis, Saarland University. http://www-wjp.cs.uni-sb.de/publikationen/St06.pdf
[61] Tanenbaum A S, Renesse R V 1985 Distributed operating systems. ACM Comput. Surv. 17(4): 419–470. ISSN 0360-0300 · doi:10.1145/6041.6074
[62] Tews H 2007 Micro hypervisor verification: Possible approaches and relevant properties. http://robin.tudos.org/publications/hyperveri.pdf
[63] The VERIFIX Consortium 2000 The VERIFIX Project. http://www.info.uni-karlsruhe.de/ verifix/
[64] The Verisoft Consortium 2003 The Verisoft Project. http://www.verisoft.de/
[65] Tsyban A 2008 Formal Verification of a Framework for Microkernel Programmers. PhD thesis, Saarland University, Saarbrücken. to appear
[66] Tverdyshev S 2008 Formal Verification of Gate-Level Computer Systems. PhD thesis, Saarland University, Saarbrücken. to appear
[67] Welch J L, Lynch N 1988 A new fault-tolerant algorithm for clock synchronization. Information and Communication 77(1): 1–36 · Zbl 0646.68029 · doi:10.1016/0890-5401(88)90043-0
[68] Yang J, Twohey P, Engler D, Musuvathi M 2006 Using model checking to find serious file system errors. ACM Transactions on Computer Systems 24(4): 393–423. ISSN 0734-2071 · Zbl 05456689 · doi:10.1145/1189256.1189259
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.