---
tags: prusti, prusti-student-projects
---

# Prusti MSc project: Secret integers, cryptography, ...

project dates: 3.10.2022 - 24.3.2023
meetings: Mondays 10:00 - 11:00 https://ethz.zoom.us/j/66748654978

## Minutes 2022-09-21

- deliverables:
- project description (first 2/3 weeks)
- final report (final 4/5 weeks)
- initial presentation
- intermediate presentation
- final presentation (shared)
- literature review + methodology (~15 pages, around halfway through the project)
- abstract
- introduction
- related work

- (previous project descriptions, for reference) https://www.pm.inf.ethz.ch/education/student-projects/completedprojects.html

- secret integers crate
- https://docs.rs/secret_integers/0.1.6/secret_integers/

- possible evaluation targets
- exponentiation vs Montgomery's ladder
- https://en.wikipedia.org/wiki/Exponentiation_by_squaring#Montgomery's_ladder_technique
- char-by-char password check
- ...
- (for amortised analysis) FIFO using two lists

- core goals
- simple (non-asymptotic) time credits
- encoding in Viper -> one "credit" == `acc(time_credit(), n/1)`, `predicate time_credit()`
- syntax, parsing for time credit annotations
- how to deal with generics?
- (ideally) as specification: `#[requires(time_credits(1))] fn foo() {}`
- as ghost argument integer: `fn foo(ghost_tc: Int) {}`
- as ghost argument with const generic: `fn foo<N: usize>(ghost_tc: TimeCredit<N>) {}`
- manual calls to `consume_credit()` (e.g. `#[trusted] #[...time_credits(1)] fn consume_credit() {}`)
- amortised time complexity
- type invariants to store time credits
- different execution models for MIR
- credits for calls + loop iterations
- credits for addition, multiplication -> secret integers
- product programs
- secrecy preservation (given different secret input, but same public input, same public result)
- review: https://pm.inf.ethz.ch/publications/EilersMeierMueller21.pdf
- evaluation

- extension goals
- inferring time credits (how to deal with loops? recursion?)
- defining credit models in user syntax