search

granule-project / granule

A statically-typed linear functional language with graded modal types for fine-grained program reasoning
https://granule-project.github.io
BSD 3-Clause "New" or "Revised" License
589 stars 33 forks source link

Security is broken #223

Closed thwfhk closed 1 year ago

thwfhk commented 1 year ago

The security (Public and Private) is broken, as we can write the following well-typed leak function.

leak : forall {a : Type} . a [Private] -> a [Public]
leak x = join (split x)

split : forall {a : Type} . a [Private] -> (a [Private]) [Public]
split [x] = [[x]]

join : forall {a : Type} . (a [Private]) [Public] -> a [Public]
join [[x]] = [x]

Fortunately, seems that this is just a bug of the implementation, instead of a bug of the semiring. I would expect join to be ill-typed as in the semiring Private * Public = Private, but obviously something went wrong during type checking.

dorchard commented 1 year ago

Thanks! I have opened a PR with the fix. This was an unfortunate conflation between two different semirings when it comes to how double unboxing behaves (which is what happens in join). This should have been defined as the multiplication for Sec, which it now is in this PR.

thwfhk commented 1 year ago

I see! Thank you.

dorchard commented 1 year ago

Fixed in dev-minor now. We will make a release with this in at some point!