Marco Patrignani

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 / Rust Rover.

[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

In the context of a PKCS#11 model learning project, we have implemented some algorithms and scripts Python [1], that are:
- An algorithm for expanding a graph with a predefined set of rules (formally, a term rewriting system),
- An algorithm for pruning said graph,
- A script to visualize such graphs using PyDot,
- A script to transform such graphs into a Boolean formula for a SAT solver.

The goal of the project is to rewrite said algorithms and scripts into a Rust library and add Python bindings so that the Rust code can be called from Python (see, for example, [2]).
The goal of the rewrite is to favor the correctness of the code and its subsequent development.

[1] https://github.com/andreastedile/pkcs11-learning
[2] https://pyo3.rs/

https://stmicroelectronics.eightfold.ai/careers/job/563637158079091?ref_src=eyJlbWFpbCI6ImFkcmlhbm8uZ2FpYm90dGlAc3QuY29tIiwiZ3JvdXBfaWQiOiJzdG1pY3JvZWxlY3Ryb25pY3MuY29tIn0.GiHu3g.rFd7mzT7hSQixAClIGOJSxcY-Jw

Supercompilation, an aggressive technique to perform partial evaluation of programs, relies on explicit program graphs and detecting equalities between vertices in this graph to stop partial evaluation.
Detection of these equalities is expensive^2.
This projects investigates if e-graphs^1, a relatively recent tool for term rewrite systems, help to improve runtime.

[1]: https://egraphs-good.github.io/
[2]: "Supercompilation by Evaluation". Bolingbroke and Jones. 2016. https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/supercomp-by-eval[…]npj/papers/supercompilation/supercomp-by-eval.pdf&type=exact

Type-based verification^1 is a powerful technique due to its inherent compositionality.
However, some existing approaches only discuss verification theoretically and do not provide a concrete implementation.
Moreover, the considered programming languages are often minimal, so realistic programs look incomprehensible to humans.
This project aims to improve the situation by implementing an elaborator^[2,3] for the existing theory.
The minimum work required would be a basic type-checker implementation relying on annotations in a given program.
Ideally, programmers need not provide detailed annotations and can use more high-level programming constructs to write their programs.

[1]: "A Fixpoint Logic and Dependent Effects for Temporal Property Verification". Nanjo, Unno, Koskinen, and Terauchi. 2018. https://www.riec.tohoku.ac.jp/~unno/papers/lics2018.pdf
[2]: "Bidirectional Typing". Dunfield and Krishnaswami. 2020. https://arxiv.org/pdf/1908.05839
[3]: "Hindley/Milner style type systems in constraint form". Sulzmann, Müller, and Zenger. 2021. https://www.academia.edu/download/40187872/HindleyMilner_style_type_systems_in_cons20151119-21055-1ka6345.pdf

Higher-Order Fixpoint Logic (HFL)^1 is a powerful tool for compositional verification of effectful, functional programs that may not terminate.
Recent approaches of program verification using HFL^2 rely on deductive rules that utilize overapproximation.
However, overapproximation inherently limits what properties can be verified.
An alternative to this invariant-based reasoning are Cyclic Proofs^3 which allow infinitely large proof trees, given some side-conditions.
In this project, you implement a cyclic proof checker for a variant of HFL(N)^4 that has potentially infinite trees.
Note that other cyclic proof checkers for certain logics exist (e.g., https://www.cyclist-prover.org/), but they do not support HFL.

[1]: "Higher-Order Program Verification via HFL Model Checking". Kobayashi, Tsukada, and Watanabe. 2017. https://arxiv.org/pdf/1710.08614v1
[2]: "Automatic HFL(Z) Validity Checking for Program Verification". Tanahashi, Kobayashi, and Sato. 2022. https://arxiv.org/pdf/2203.07601v1
[3]: "Software Model Checking as Cyclic Proof Search". Tsukada and Unno. 2021. https://arxiv.org/pdf/2111.05617
[4]: "A Cyclic Proof System for HFL(N)". Kori, Tsukada, and Kobayashi. 2021. https://arxiv.org/pdf/2010.14891

Program verification is costly; but protocol verification works relatively well. SPECMON monitors an application's interaction with a cryptographic library and the network, forcing it to comply with a protocol model written in Tamarin. Ideally, this model is proven secure; SPECMON then enforces that the application either follows the model, or is aborted.

    SPECMON is not yet able to deal with applications that are malicious, i.e., try to circumvent the monitor, because of _exfiltration_: an application can encode secrets, e.g., keys, in payload messages, so that a third party learns them. In general, it is impossible to recognize keys, as they can be encoded arbitrarily. The next best thing is to hide the secret from the application in a way that (a) does not bother honest applications, (b) does not bother communication partners and (c) does not give useful information to the application. Thought experiments tell us that this is possible for some protocols, but not all of them.

    The goal of this Master's thesis is hence to
    1. Devise a systematic way to hide secrets from the application.
    2. Model this strategy as a translation from a Tamarin model of an honest application to a Tamarin model of a dishonest application with the secret-hiding monitor.
    3. Apply this translation to some well-known protocol examples and see which protocols can be monitored against malicious applications.

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.

SPECMON [CCS'24] is a monitor that ensures a programs compliance to a protocol specification in Tamarin's input format, so properties proven in Tamarin also apply to the implementation. The program is seen as a black box; SPECMON only cares about the interaction with the OS (network input and output) and some crypto library it uses. Currently, a malicious program can "cheat" SPECMON, by sending its secret via some part of the protocol to a third party (e.g., encoded within a message in a chat protocol). To circumvent this, we want to (a) encapsulate the program in a WASM sandbox and (b) modify the library and monitor so the program gets a different version of the secret than is actually used. 

This macro-project has several focus: 
1) a very fast implementation [bachelor + intership], 
2) an evaluation of the security of point b) with several programs [bachelor + intership; masters], 
3) a mathematical proof that the library substitution ensures that secrets remain secret and honest applications behave no different with the substitution in place [masters].
 

Sapic+ is a protocol description language [1].
The goal of this project is to define modules (or packages), a modules system and modules composition for Sapic +.
These operands need to be proven correct wrt Axioms 5,6,7 in this work [2].
 

The goal of this project is to study the security of cryptographic keys managed in CIE (carta di identita` elettronica) by the implementation of the PKSC11 standard.
There are some known attacks, that we'll start by replicating, and then move on to find new ones.

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/

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 

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.