---
# System prepended metadata

title: 'Prusti MSc project: Secret integers, cryptography, ...'
tags: [' prusti-student-projects', prusti]

---

---
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
