Exercise sheets

I have posted the fourth set of exercises for you, and selected solutions to exercises from this week's exercise sheet.

Seminar on Tuesday, 4 November

The first hour of the exercise session on Tuesday, 4 November, will be devoted to a seminar by Arnar Birgisson (School of Computer Science, Reykjavík University, Iceland). You are all strongly encouraged to attend the talk!

Title: Enforcing Authorization Policies using Transactional Memory Introspection

Abstract:
Correct enforcement of authorization policies is a difficult task, especially for multi-threaded software. Even in carefully-reviewed code, unauthorized access may be possible in subtle corner cases. We introduce Transactional Memory Introspection (TMI), a novel reference monitor architecture that builds on Software Transactional Memory—a new, attractive alternative for writing correct, multi-threaded software.

TMI facilitates correct security enforcement by simplifying how the reference monitor integrates with software functionality. TMI can ensure complete mediation of security-relevant operations, eliminate race conditions related to security checks, and simplify handling of authorization failures. We present the design and implementation of a TMI-based reference monitor and experiment with its use in enforcing authorization policies on four significant servers. Our experiments confirm the benefits of the TMI architecture and show that it imposes an acceptable runtime overhead.

The work has just been presented at the 15th ACM Computer and Communications Security Conference (CCS 2008), 28-31 October, Alexandria, VA, USA.

First Exercise Solution from Group 8

The proposed solution is here. The author and I look forward to your comments.

Miniproject for the Course

I have posted the miniproject. I strongly encourage you to start working on the project as soon as possible, even though the deadline for the delivery of your work is on Friday, 14 November.

Keep up the good work!

Solution from Group 2

The solution from group 2 is now available here. Group 4 is expected to post their comments on this solution on the blog by Wednesday, 29 October, at 12:00 CET. Other groups are, of course, welcome to provide feedback and suggestions for improving the solution.

Commenting on the Solutions

Based on the solutions I have received so far, I expect the following groups to comment on each other's exercise solutions:

• Groups 1 and 3,
  
• Groups 5 and 6.
  

Post your comments on the blog by Wednesday, 29 October, at 12:00 CET. Other groups are, of course, welcome to provide feedback and suggestions for improving the solutions.

Posting of Exercise Solutions

The easiest way for you to post your solutions to the exercises is to send me the source and pdf files via email. I will then take care of making the solutions available from the web.

Keep up the good work!

Solution to the exercise 3.6

Here's the solution + latex sources.

New Groups

Group 7: Giordano Bitunni and Nicola Ruffini.
Group 8: Alessandro Bettacchi

Group 7 should post a solution to Exercise 3.17 (part 1) in the text book. Group 8 should post a solution to Exercise 3.17 (part 2) in the text book.

The solutions are due by Tuesday, 28 October at 12:00 CET.

LaTeX File Template

You can find an example LaTeX file, with some macros you may find useful, here. The file generates the solutions to the exercises for the first session, so that you can see what the source produces and learn how to use the macros that way.

Latest on Exercise and Project Groups

Nico Paoletti has joined group 3.

In addition, there are two new groups.

• Group 5: Aureli and Falcioni.
• Group 6: Francesconi and Papalini.
  

Groups 5 and 6 should post solutions to the two items in Exercise 3.13. Group 5 should answer the question related to restriction, and Group 6 the one related to relabelling.

First Call for Exercise Solutions

Exercise group 1 should post on the blog their solution to Exercise 2.10 in the textbook.

Exercise group 2 should instead post their solution to Exercise 2.11 in the textbook.

Exercise groups 3 and 4 should instead post their solutions to Exercises 3.6 and 3.7, respectively.

All solutions are due by Friday, 24 October, at 12:00 CET. Solutions should be provided in pdf and source LaTeX.

Exercise and Project Groups

Based on the information you have sent me so far, I am aware of the following exercise and project groups. Drop me a line if you are following the course and you are missing from the list below, so that I can update the "official" list and start assigning exercises to each of the groups.

• Group 1: Andrea Caputo and Daniele Fanì.
• Group 2: Marco Dezi, Stefano Ficcadenti and Roberto Mindoli.
• Group 3: Andrea Baiocco, Luca Micozzi and Michele Manzotti.
• Group 4: Danila Leonori, Guðrún Fema Ólafsdóttir and Talia Tiberi. (Danila, Guðrún and Talia, since you expressed no preferences regarding your exercise and project group, I decided to put the three of you together. Of course, you should feel free to complain if you disagree.)
  

Watch this space for upcoming exercise assignments.

Modelling Exercise Using Labelled Transition Systems

Define an LTS describing the behaviour of a vending machine that obeys the following constraints.

• The vending maching can dispense coffee, tea and chocolate.
  
• Coffee costs 20 cents, tea costs 10 cents and chocolate costs 20 cents.
  
• The machine accepts 10 and 20 cent coins.
  
• The machine never makes a profit and does not give change.
  

Try not to impose other restrictions on the behaviour of the vending machine.

Update on Student Activity on the Course Blog

I suggest that the students attending the course form "working groups" during the first week of the course. By Wednesday 15 October at 12:00 I'd like to receive an email from each group of two or three students telling me who the members of the group are. The group will work together throughout the course.

Each group of students is expected to post their solutions to selected exercises from the textbook in the form of a PDF file accompanied by the LaTeX source for the file. The other groups are expected to contribute comments on each solution that is being presented by their colleagues. The contributing group will then have to improve their solutions taking the comments they receive into account.

If they are of sufficient quality, the solutions you will give to the exercises will, with due attribution, be part of a "teacher's handbook" that my co-authors and I will make available here. Do a good job and some famous people will be forever grateful to you :-)

I will assign the exercises to the groups on a weekly basis.

Test Post

This blog will be used for the Modelling and Verification course that I will be holding in Camerino, Italy, over the next couple of months.

Students in the course are expected to be active on the blog, posting questions to each other, providing answers to them and commenting on the answers that have been provided by others. Activity on the blog will account for 5% of the final mark for the course.

Whenever you write a post on the blog, you should

• be as clear as you possibly can,
  
• be courteous in your writing,
  
• proof read what you write, and
  
• overall take pride in what you write.
  

Remember that being able to express your ideas, questions and solutions in writing is a skill that you will need in the future regardless of what your future occupation will be.

I hope that you will enjoy using the blog and following the course.