Marco Patrignani

Spectector [1] is a symbolic analysis tool for programs detecting speculative leaks. We are working on a verified version in the proof assistant Coq [2].
Coq has an extraction mechanism to OCaml [3] and we would like to have the command line interface of Spectector in Ocaml calling the extracted code.

Furthermore, Spectector parses assembly files into their language muasm and we would like to re-use the front-end of Spectector.
The first goal of this thesis is to use Menhir [4], a parser generator that also outputs coq code, to parse the output muasm output of Spectector. This is done by specifying the grammar of muasm in a specific notation used by Menhir which then automatically generates the parser.

The next goal is to write a command line interface in Ocaml replicating the most important Spectector flags and calling the appropriate functions in the extracted Ocaml code.

Below we have outlined a roadmap of different steps that will be important during the project:

  - [ ] Write a parser in OCaml that takes parses the provided user program using Spectector. Thus, the program is first given to Spectector to be parsed (Spectector -a none shows the parsed file) and take this output to the Ocaml parser to parse into the structure expected by the extracted Ocaml analysis.

  This means to generate a Program of the $\mu$asm AST defined in Ocaml.

    - [ ] Familarize yourself with Spectector format and parse some files to Spectector

    - [ ] Write an initial parser for a subset of the constructs in the language ($\mu$asm right now does not define all constructs)

    - [ ] However parse all of them. Especially the call constructs with the callstart and retstart constructs. These should map back to single call instructions.

    - [ ] Spectector has the option to parse unsupported instrucions. Do we want to reflect this as well or stop in the parser? Or have an error node and report it to the user.

    - [ ] The specification of $\mu$asm is just one datatype in Ocaml.

    - [ ] Similar to expressions. Expressions only contain Add, Sub and Mul right now. If the need arises, please extend the expr data type of the extracted Ocaml but give a warning or option to give a warning if such an extended construct is used.

- [ ]  Write a command line Interface in Ocaml that mimics the Spectector command line. Furthermore, this includes writing glue code that wraps corresponding functions like expand to include for example a step count or a timeout.

  Wrapper is important here, since the extracted function may change with the development. We keep trying to let the types be stable.

  - [ ] This project could include helper functions like creating the initial states in Coq

  - [ ] Only the most important options like:  

    -  -n -s to use non-spec or spec respectively.

    -  -w Size of speculation window

    -  -a analysis option.

    -  -t -s timeout and steps (need to be implemented in Ocaml)

    -  and any other interesting options.

   -  Furthermore, bindings to invoke off-the-shelf SMT solver?

### References:

- [1] https://github.com/spectector/spectector

- [2] https://coq.inria.fr/

- [3] https://ocaml.org/

- [4] https://gallium.inria.fr/~fpottier/menhir/

Timesheets are monthly report where personnel must report their activities for a specific project, and how many hours they worked on that project.

Filling out timesheets is a boring administrative task that we want to automate.

The goal of this project is to create a bot uses an LLM of choice to learn what task a researcher is working on, in a specific project.
Then the bot should fill out the timesheet automatically, counting the correct amount of hours and extracting reasonable text from the project description (which should be provided by the user) via the LLM interaction.
This project should also reverse-engineer the unitn timesheet website to understand the hppt requests in order to supply the bot product directly to the timesheet university application.

Flowistry is a tool that analyzes the information flow of Rust programs [1,2] that currently exists as a VSCode plugin.

The goal of the project is to port this plugin to Clion.

[1] Modular Information Flow through Ownership. Will Crichton, Marco Patrignani, Maneesh Agrawala, Pat Hanrahan. https://arxiv.org/abs/2111.13662

[2] https://github.com/willcrichton/flowistry

Universal composability (UC) [1] is the gold standard for the security of any cryptographic protocol.

Recent results show that in order to prove that a protocol is UC, it is sufficient to prove trace equivalence between the protocol and its ideal functionality [2].

The project consists of taking the wireguard protocol [3] and prove it is trace equivalent to its functionality using the Deepsec tool for testing trace equivalence.

[1] https://en.wikipedia.org/wiki/Universal_composability
[2] https://arxiv.org/abs/1910.08634
[3] https://www.wireguard.com/ papers/wireguard.pdf

Spectector is a tool for the automatic analysis of multiple Spectre attacks [1].
Currently, Spectector requires the whole program for its analysis to run, that is, you need to provide any library and any 3rd party software that your code calls.
This known problem in software analysis can be bypassed in many ways, and [2] can serve as a background starting point.
The goal of this project is to make Spectector modular, that is, if you want to analyse a piece of code C that relies on some library L, you should provide additional annotations for the places where C interacts with L, but you should not provide the code of L.

[1] https://github.com/spectector/spectector
[2] https://oar.princeton.edu/bitstream/88435/pr1sk1h/1/AutomatingModularVerif.pdf 

please see the italian description.

Actum [1] is a novel and under development library in Rust for implementing fault-tolerant actors [2] which takes inspiration from Akka. The goal of this project is to contribute in the development of the distribution capabilities of Actum. This concerns:

• Understanding the motivations of distributed actor systems (also known as actor clusters).
• Studying how existing actor libraries such as Akka [3], Coerce [4] and ractor [5] implement distribution. At a theoretical level, you will at least face the concepts of gossip, failure detection, event ordering, leader election.
• Implement the required features to achieve distribution (or parts of them).

[1] https://github.com/andreastedile/actum
[2] https://en.wikipedia.org/wiki/Actor_model#Fundamental_concepts
[3] https://doc.akka.io/docs/akka/current/
[4] https://github.com/LeonHartley/Coerce-rs/
[5] https://github.com/slawlor/ractor

Universal Composability (UC) is the gold standard for proving that a cryptographic protocol is secure [1], by proving that a (complex) protocol is equivalent to a (simpler) functionality. Different flavours of UC exist: perfect and computational, with different security implications.

Many research papers prove UC for various protocols. In order to develop further research, we need to have a thorough list of what works prove what kind of UC for what protocols, and if there exist different protocols that are proven UC with respect to the same functionality (for example, Canetti and Fischlin's commitment [2] and Lindell's commitment [3] both use the same functionality).

[1] https://en.wikipedia.org/wiki/Universal_composability
[2] https://eprint.iacr.org/2001/055.pdf
[3] https://eprint.iacr.org/2011/180

The Sanbapolis Arena has 13 cameras deployed to record sport events from multiple perspectives. 

The goal of this project is to allow the teams to extract various analytics from the past stream as well as from the live stream of the arena.
Different analytics rely on detection of: balls/court/players/positions.
Different analytics will be sport-specific, so we expect to meet with people from the teams that train at Sanbapolis in order to understand their needs.

The Sanbapolis Arena has 13 cameras deployed to record sport events from multiple perspectives. 

The goal of this project is to rewrite the simple recording functionality that directs the cameras in order to provide the various teams with the recordings. Currently the functionality is in python, we want a more robust an maintainable language for the infrastructure.

Universal composability (UC) [1] is the gold standard for the security of any cryptographic protocol.

Recent results show that in order to prove that a protocol is UC, it is sufficient to prove trace equivalence between the protocol and its ideal functionality [2].

The project consists of taking the single-bit commitment of Lindell [3,4] and prove it is trace equivalent to the commitment functionality using the Deepsec tool for testing trace equivalence.

[1] https://en.wikipedia.org/wiki/Universal_composability

[2] Patrignani, Wahby, Künnemann: Universal Composability is Secure Compilation. https://arxiv.org/abs/1910.08634

[3] https://eprint.iacr.org/2011/180.pdf

[4] https://eprint.iacr.org/2013/123.pdf

The goal of this project is to take the rust PBFT implementation and add support for Creusot [1].

[1]: https://github.com/xldenis/creusot

If you have taken the semantics class, or if you are interested in programming languages semantics, there are a number of research projects ranging from smaller-to-bigger in the field of programming languages and semantics (applied to security).

Given the requirements on your background, please come talk to me/send me a mail if you are interested.

Do you have a cool idea about something to be done in Rust?

Are there existing crates with open PRs that require substantial amount of Rust-work and that interest you?

Good.

Come talk to me about that and we'll see whether it is thesis material or not.