Homework (Week 7) Term 2, 2020 Announcements Course Outline Course Schedule Glossary Maths Resources Moodle - BB Collab Piazza Forum Assignment 0 Spec TeX Guide Web Submission Assignment 1 Spec TeX Guide Web Submission Assignment 2 Spec Web Submission Java Resources Monitors Video Multithreading Video Semaphores Video Volatile Video Web Tutorials Week 1 Homework Monday Board Recording Slides Condensed Slides Thursday Code Slides Condensed Slides Week 2 Homework Thursday Slides Condensed Slides Week 3 Homework Monday Brownies Promela Samples Slides Condensed Slides Thursday Code Slides Condensed Slides Week 4 Homework Monday Slides Condensed Slides Thursday Slides Condensed Slides Week 5 Homework Monday Slides Condensed Slides Thursday Slides Condensed Slides Week 7 Homework Monday Slides Condensed Slides Thursday Slides Condensed Slides Week 8 Homework Monday Slides Thursday Slides Week 9 Homework Monday Slides Thursday Slides Week 10 Notes Homework (Week 7) Table of Contents 1. Non-compositional Verification 2. Compositional Verification Submission: Due on Thursday, 23rd of July, 6pm Sydney Time. Please submit using the CSE Give System either online or via this command on a CSE terminal: give cs3151 hw6 hw6.pdf
Please put all your answers in one PDF file called hw6.pdf. Use of LaTeX is encouraged but not required. Please make your answers as concise as possible. This homework should not be more than two pages, and preferably no more than one. 1 Non-compositional Verification Here is a three process message passing system presented as a transition diagram of three processes \(P_1\), \(P_2\), and \(P_3\). Prove using the Levin and Gries or AFR methods that the following Hoare triple holds: \[ \{ \textsf{True} \}\ P_1\ \|\ P_2\ \|\ P_3\ \{ y = v - 1 \}\] 2 Compositional Verification Assume we have a function \(\textsf{encrypt}(k,v)\) which given a byte \(v\) returns an encrypted version of the byte using the key \(k\), and that there is a function \(\textsf{decrypt}(k,v)\) that is defined such that \(\textsf{decrypt}(k,\textsf{encrypt}(k,v)) = v\). A sender process wishes to transmit an array of bytes \(A\) of length \(N\) to a reciever process which will store the bytes into a result array \(B\). However, the array of bytes is top-secret information that should not be shared on a public channel. There are two synchronous channels that connect the two processes, one public (called \(P\)) and one secret (called \(S\)). The secret channel is expensive and can only be used for one message to transmit the key. Therefore the array of bytes must first be encrypted and then transmitted over the pubic channel. Construct synchronous transition diagram for the sender and receiver. Devise a suitable postcondition for the parallel composition of these processes. This involves two components: Stating that the contents of \(B\) should be the same as \(A\). Stating that no secret data was transmitted on the public channel. You may assume some predicate \(\textsf{Secure}(v)\) that is only true for encrypted data. Prove your program correct using the compositional method. Prove deadlock-freedom. 2020-08-06 Thu 03:32 Announcements RSS
