Outline and materials
Lecture 1: main issues in the field, discussion
complexity of the artifacts (software, networks , ...) allowing abuses (with fantasy from the attackers)
economy and crime (no more “War Games”-like underground heroes)
trending risks, an example: Bring Your Own Device
overlap between security and Privacy/Rights (MY data on computers, attacked by criminals or agencies)
Lecture 2: low level vulnerabilities
wrongly using signed instead of unsigned int in C-language Linux kernel: “Linux Kernel CVE-2013-2094 Local Privilege Escalation Vulnerability ”:
the vulnerability description (and exploit) on securityfocus.com/bid: http://www.securityfocus.com/bid/59846
its first discovery: http://lkml.iu.edu//hypermail/linux/kernel/1304.1/03652.html
using the LCA fuzz tester: http://lwn.net/Articles/536173/
the description of the possible abuses: https://bugzilla.redhat.com/show_bug.cgi?id=962792#c16
the very simple patch;
the “NULL pointer dereference “ vulnerability:
its description: http://cwe.mitre.org/data/definitions/476.html
a lengthy but complete discussion: https://blogs.oracle.com/ksplice/entry/much_ado_about_null_exploiting1
a specific occurrence of this kind of vulnerability, in the Linux kernel: https://www.cr0.org/misc/CVE-2009-2692.txt
its description: http://www.securityfocus.com/bid/36038
the (again) simple patch;
Lecture 3: CLIPPER, Trusted Computing
the story of the US-goverment-backed CLIPPER chip: http://www.cryptomuseum.com/crypto/usa/clipper.htm
the paper describing CLIPPER's weakness: M.Blaze “Protocol Failure in the Escrowed Encryption Standard ” 1994 (PDF)
the proposal of the TPM chip by the TrustedComputingGroup.org (TCG): Section 4.2 of the TPM design document
a paper discussing a vulnerability of a protocolo defined by the TCG: Bruschi,Cavallaro,Lanzi,Monga “Replay Attack in TCG Specification and Solution ” (PDF)
Lecture 4: a vulnerability in Android, a checker for “buffer overflow”
cryptografical signing of applications defeated by unzip libraries: the “Android Master Key” vulnerability, and exploit: http://www.saurik.com/id/17
checking against “buffer overflow” vulnerability in C-language source code:
the Boon checker, the paper by Wagner,Foster,Brewer,Aiken describing it (PS)
Lecture 5: two other checkers
the general checker obtained in Stanford by extending the GCC compiler (and which became the Coverity company):
a first paper by Engler&al., a second paper by Ashcraft&Engler
using high logic for low level memory heap/pointers management: “Compositional shape analysis by means of bi-abduction”:
the paper by Calcagno,Distefano,O’Hearn,Yang: Journal of the ACM, 58-6 p.26, 2011 (draft PDF)
applications of this approach: PDF
(interesting: a whole course on this: http://depend.cs.uni-sb.de/?512 )
Lecture 6: introduction to model checking
representing systems and their behavior: Kripke structures
representing systems' properties to be checked: Linear Temporal Logic
Lecture 7: model checking with SPIN, checking a protocol
about the SPIN model checking tool (from slides by S.Schwoon)
the Needham–Schroeder Public-Key Protocol, for mutual authentication: see section in http://en.wikipedia.org/wiki/Needham%E2%80%93Schroeder_protocol
model checking overview, and checking Needham-Scroeder with SPIN: see pages 1 to 28 in http://www7.in.tum.de/~esparza/Talks/slides-maratea.pdf
(an interesting lecture on model checking: http://www.uio.no/studier/emner/matnat/ifi/INF5140/v09/undervisningsmateriale/09-claims.pdf )
Lecture 8: closing (thu. 6 march 2014 h.10(NEW!), “Sala Seminari”)
topics, or problems, for the short final report or presentation
further trends in computer security (Cloud, ...)