Formal Methods in the Software Life Cycle
[
main |
cases |
smart cards |
formal methods |
schedule |
groups
]
Week 1
- Lecture:
Monday April 23, 10.00 - 11.45.
General introduction.
Formal methods for security protocols.
Smart cards.
- Feedback:
- Assignment:
- Groupwise, start working on your case. Eg:
- Think of use cases (scenarios), and the terminal(s) involved.
- Think of the security requirements
- Find a suitable protocol. Which keys will you need, in the terminal and/or on the smartcard?
Begin preparing a 5 to 8 page document describing concisely
the project plan for the applet and terminal(s) for your case.
Short and sweet is preferred over long and unwindly.
The document should briefly describe what the whole system will do.
Imagine you're presenting the system to some company/country that
might want to use it for their customers/citizens.
Also include some more technical details about
- data that is stored on- or off-card,
- the cryptographic keys that will be used, on the smartcard
and/or in the terminal(s), and
- if this is already clear to you, the protocol that will be
used to communicate between terminal and smartcard
- Groupwise, get the
example applications -
Chipknip, Table and Calculator - running on the smartcard hardware.
- Individually, think about and look for an inspiring topic for your
essay
based on a paper from
Cardis'06 (LNCS 3928),
Cassis'05 ( LNCS 3956) or
Smart Card Programming and Security (LNCS 2140).
- Smart Cards:
Jing Pan will distribute smartcards, readers and software on Tuesday afternoon.
Week 2
- Lecture:
Tuesday May 1, 10.00 - 12.30.
Introduction JML. ESC/Java.
- Assignments:
- Prepare groupwise a 5 to 8 page document describing concisely
the project plan for the applet and terminal(s) for your case.
Short and sweet is preferred over long and unwindly.
Have it delivered in format to Erik Poll
by 9:30 am, Tuesday May 8.
- Also remember to sent the paper proposal for your essay in format to Bart Jacobs by 9:30 am, Tuesday May 8.
- ESC/Java homework assignment
Send it to Wojciech Mostowski before 9:30 am, Monday May 7.
- Consultancy hours:
Thursday May 3, 11:00. This is specifically meant for your
ESC/Java2 exercise, so get working on this before Thursday.
Week 3
- Lecture:
Monday May 7, 10.00 - 12.30.
Java Card.
RMI.
Applet lifecycle and protocol states.
- Slides Java Card (1up)
(6up)
- Slides Modeling Applet Life Cycles and Implementing Protocols
(1up)
(6up)
The paper "Implementing a formally verifiable security protocol in Java Card"
gives some idea on how to move from an abstract security protocol to a concrete implementation in Java Card, specified in JML.
The paper "Systematic Development of Java Card
Applets" also presents how OCL state diagrams can be used to develop communication protocols for Java Card applets.
- Assignment:
Get working on your case! Some hints on how to start:
- Think about the different terminals needed.
- For each scenario in which the smartcard interacts with one of the terminals, think of the security requirements and design a suitable protocol. Which keys will you need, in the terminal and/or on the smartcard ?
- Lay down the protocols used.
- Implement the Java terminal(s) and the JavaCard applet,
and specify them using JML.
Ultimately, we want you to check the Java Card applet
with ESC/Java2, and the terminal with the runtime assertion checker.
- Consultancy hours:
Wednesday May 9, 10:00-12:00
Week 4
- Lecture:
Tuesday May 15, 10.30 - 12.30.
Java Cryptography API.
JML runtime checker.
Some more JML and ESC/Java2 hints & tips.
- Consultancy hours:
Wednesday May 16, 13.45 - 15.45.
We will also have short meeting with each of the groups to discuss progress, problems, etc.
Week 5
- Consultancy hours:
Monday May 21, 10.00 - 13.30.
- Consultancy hours:
Wednesday May 23, 10.00 - 12.30.
Week 6
- Final presentation:
Wednesday May 30, 10.00 - 12.30.
Each group gives an overview of their application and
a demo showing its working (25 minutes in total).
Maybe you can briefly mention the highlights and/or lowlights of your
experiences with the formal methods and tools.
- Final deliverable of each group:
due Monday June 4.
-
Document of 8 to 12 page discussing the influence of the formal modelling
on the design and implementation of your application.
Note that this means you shouldn't try to give a detailed description of
your application, but we want you to focus on your conclusions about how the
formal methods and tools did - or did not - play a part in the design
and implementations: what were tools good for, what were they not good
for, where did the methods and tools help, etc. ?
- JML-annotated source code --
gzipped tar file of all class files including comments and
annotations.
- Indivually:
8 to 12 page
on a topic related to formal methods.
Due Tuesday June 5.
Hand in of final document, essay (txt, ps or pdf, hence NO doc) and
sources via e-mail to Erik Poll, erikpoll(at)cs.ru.nl with a cc to
Wojtek, woj(at)cs.ru.nl.