Fysikkbygningen øst (kart)
Sem Sælands vei 24
Master topics which use SMT technology for optimization and verification problems in planning and program verification. Several different topics are possible.
The work of Bjørnar Luteberget, Koen Claessen (from Chalmers), and Christian Johansen (from PSY and ConSeRNS groups at IFI) won the Best Paper Award at the 18th Conference on Formal Methods in Computer-Aided Design (FMCAD), which was held in Texas, USA, in November 2018.
This topic involves understanding and modelling the election management algorithm Sainte Lagues, which is developed/maintained by UiO people (students and researchers led by Bernt Aardal). Moreover, the topic involves working with verification techniques and tools, both for algorithms but also for code. The programming language is TypeScript.
You are interested in security protocols. Ceremonies are a new view which extends security protocols by integrating the human factor in the picture, as well as looking at the security protocol/system in entirety, making the assumptions explicit and composing several protocols for communication and security in the same analyses.
There are very few tools and formalisms for ceremonies, therefore you will have a lot of freedom. You will investigate and build a tool for ceremonies based on an existing tool for security protocols. You will investigate graphical languages and code generation, or you can look into how to analyze ceremonies.
This project involves looking into Bitcoin or Etherium and the protocols and security technology behind it. You should expect to work with newly introduced technologies like Bitcoin consensus and distributed peer-to-peer network algorithms, or Block-chain style of distributed write-only database, or proof-of-work algorithms.
Depending on the motivation and abilities of the student, this project include work on developing a new Crypto-currency for Science, which is a project initiated by Stefan Krauss.
by Lars Tveito
Real-time collaboration allows multiple users to view and edit a document simultaneously over a network. In this thesis, we develop a new protocol, called Shared Buffer, which enables real-time collaboration in existing editors. Shared Buffer leverages a client-server architecture and minimizes the implementation effort of the client-side algorithm. It achieves this without degrading the responsiveness of the editor.
The greatest challenge of a real-time collaborative system is ensuring consistency between the distributed copies of the document. We chose eventual consistency as the consistency model, which essentially states that if all users stop typing, then eventually they will look at the same document.
We apply a formal verification technique called model checking, using it as a tool to validate the protocol. The behavior of the system is formally specified in Maude, a language based on equational and rewriting logic. Linear Temporal Logic (LTL) is used to formalize the consistency model. Using the Maude LTL model checker, we have verified that the system exhibits eventual consistency for a limited number of clients and operations.
A Shared Buffer server has been implemented in Clojure, a modern functional language with strong support for concurrency. Client implementations have been developed as an extension for Emacs, a widely used text editor, and as a library for the Python programming language.
The work of Bjørnar Luteberget, Christian Johansen, and Martin Steffen (from PMA and ConSeRNS groups at IFI) won the Best Paper Award at the 12th International Conference on Integrated Formal Methods, which was held in Iceland in June.
Depending on the motivation and abilities of the student, this project can include a one semester exchange with IT University of Copenhagen. This project could also involve interaction with the Norwegian ministry of local government and modernization, which is taking care of implementing eVoting in Norway.