This is the moodle course site for the lecture "Formal Specification and Verification of Object-Oriented Software"

Foundations of reliable distributed systems (DSs), including failure and system models, and communication and agreement problems. 

- Basic concepts and definitions (e.g., system models, failure models, time) 
- Group communication with crash failures (e.g., failure detectors, consensus, membership) 
- Crash recovery and Byzantine failures (e.g., Paxos) 
- Data replication, scalability (e.g., quorum systems, distributed storage systems) 
- Distributed transactions and commit (e.g., Two- and Three-Phase Commit, Non-blocking Atomic Commit) 
- Consistency (e.g., linearizability, causal consistency, strict serializability) 
- More hard problems (e.g., leader election, uniform reliable broadcast, terminating reliable broadcast) 
- Programming support for reliable DSs (e.g., Pi calculus,  and behavioral typing, debugging, model checking)



Formal methods allow one to model critical requirements precisely and to certify with mathematical rigor that such requirements are met by a system. For applying formal methods to real world problems, tool support is essential. This lab course introduces how to use the Isabelle/HOL tool that is one of the internationally leading tools. Formal models of increasing conceptual complexity will be defined in Isabelle's higher-order logic, so that Isabelle's semi-automatic verification engine may subsequently be used to verify the desired properties. The topics covered by this course include:

  • techniques for modeling systems in higher-order logic,
  • techniques for specifying desired systems properties,
  • design of formal models for systems,
  • evaluation of advantages and disadvantages of a chosen model,
  • techniques for conducting semi-automatic proofs in Isabelle/HOL.


Prerequisites

Knowledge of Computer Science and Mathematics, equivalent to the first four semesters in the Computer Science Bachelor program, in particular ability to work with formal languages and calculi, and knowledge of propositional and predicate logic.


In this lab course, we implement a realistic tool that will allow us to reliably detect leakage of private information on Android smartphones. The lab will cover the following topics:

  • we investigate the problem of information leaks in detail
  • we consider languages for defining privacy requirements
  • we formally define an analysis for finding leaks in Android applications
  • we implement this analysis in a tool

The course Network Security covers the principles and practice of computer and telecommunication network security with particular emphasis on Internet security. After transferring the fundamentals of IT security and cryptography to the networking domain, we follow a top-down approach to network security. Starting with the application layer, the course provides a detailed discussion of network security principles and protocols. In addition to well known mechanisms, recent developments in the area of network security (e.g., peer-to-peer security, mobile network security, etc.) will be thoroughly examined. Further static course information can be found on the SEEMOO homepage.

The course deals with cutting edge development topics in the area of network security with particular focus on mobile networked systems. Beside a general overview it provides a deep insight into a special development topic. The topics are selected according to the specific working areas of the participating researchers and convey technical and basic scientific competences.

In this seminar, we will discuss recent research papers covering pitfalls and solutions for secure usage in mobile devices. Each paper will be presented by one participant of the seminar and will then be discussed intensely by the entire group of participants.

The papers of the seminar are clustered in three areas:

  • Access Control Mechanisms
  • Usage Control Mechanisms
  • Security Analyses of Data and Resource Usage

The papers in each area consider operating system level or application level mechanisms, current vulnerabilities in mobile devices and special considerations for usage control on mobile devices.

The Seminar as well as the Advanced Seminar on Networking, Security, Mobility, and Wireless Communications cover current research in the given topic areas. Under supervision of the tutors, the seminar includes studying, critically analyzing and discussing, summarizing, and presenting selected research articles. Deliverables are a short presentation, a final presentation, and a seminar paper. The Advanced Seminar additionally emphasizes on the entire research process.