Figure out how to express "timing" for constant time assignment(s)

[dbp]

We had an assignment last year, that I'd like to do in some form:

Here in the current version: (not a particularly stable url) https://courses.dbp.io/logics24/hw3a.html#(part._.Problem_3)

Essentially, they are given a not constant time password checking function, are asked to write a spec that verifies that, and then fix the code. Because timing really requires sampling, and I didn't have an easy way to do that, I simulated the time with a "clock tick" mutable ref. This meant, of course, they had to use specific functions that incremented that, but seemed to work okay.

Either we should figure out a better way of doing this (@camoy mentioned using allocations as a proxy for time, or really, change the problem to constant space; wonder if that still requires sampling), which maybe means having some ability to sample?

Or should just build in the same functionality as I had last year.

[camoy]

I did a quick test and this ticks function should be good enough for our purposes:

(define (ticks thk)
  (define before (current-memory-use 'cumulative))
  (thk)
  (define after (current-memory-use 'cumulative))
  (- after before))

Just doing a couple experiments, if you correctly implement check-password without timing leaks, you'll get either exactly the same number of ticks or a few hundred off. The leaky version can have way more ticks in the worst case (can be like 2x more), so that's easily detectable.

[dbp]

Great!

On Dec 18, 2023, at 3:19 PM, Cameron Moy @.***> wrote:

I did a quick test and this ticks function should be good enough for our purposes:

(define (ticks thk) (define before (current-memory-use 'cumulative)) (thk) (define after (current-memory-use 'cumulative)) (- after before)) Just doing a couple experiments, if you correctly implement check-password without timing leaks, you'll get either exactly the same number of ticks or a few hundred off. The leaky version can have way more ticks in the worst case (can be like 2x more), so that's easily detectable.

— Reply to this email directly, view it on GitHub https://github.com/logiccomp/lsl/issues/3#issuecomment-1861536772, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAELBJJBYU5TP7JICRJTGILYKCQMPAVCNFSM6AAAAABAZ5YF2SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQNRRGUZTMNZXGI. You are receiving this because you authored the thread.