mathetic

hace 5 añosdiscuss

Sorry, I didn't mean to mislead. I was exemplifying ways of subtly leaking data. In the next paragraph, I clarify what we cover with the following:

> Namely, we implement a type system that regulates explicit and implicit dataflows as well as non-termination as a covert channel.

Yes, there is work on preventing timing attacks using static types. One is "A Hardware Design Language for Timing-Sensitive Information-Flow Security" which addresses exactly this problem. The second line of work is resource analysis. There are type systems that can specify the complexity of the program. Check out for example relational cost analysis [0]. This can be used for privacy and security purposes.

Needless to say, this is considerably more sophisticated than what I covered.

[0] https://dl.acm.org/doi/10.1145/2694344.2694372 [1] https://dl.acm.org/doi/10.1145/3009837.3009858

mathetic

hace 5 añosdiscuss

I used natural numbers as a simplification. In full generality, you can use a lattice where min and max are replaced by meet and join operations. Then you can have categories that are not comparable to each other.

As for privacy, you definitely have security levels. For example, think of employee record system in a simple company. The employee, payroll, human resources, and general public (perhaps accessing the system through the public-facing portion of their website) will all have different levels of access to information. You probably have the following lattice of access.

          employee
       /           \
      /             \
  payroll        human resources
     \              /
      \            /
          public

These security levels would make sense because public would have the least access (public bio perhaps), payroll would need access to things like your salary, human resources would need access to a record of disciplinary action, and you'd have access to all the information as you probably inputted most of it. This is one of many possible structures a company might have. I'd argue access to employee information is definitely a matter of privacy.

That said you're right that there is a dynamic nature of this discussion. What happens if access depends on my geographic location? That information will be stored in a database. This information is dynamic, but you can still use static checking. It'd look something like the following:

  location := getLocation(usedID);
  match location with
  | UK -> ...
  | US -> ...

Now, you don't know what location you have, but once you pattern match on it, you can check `...`s according to the correct level statically because you know that you can never execute that code if the location was elsewhere. So we use dynamic checks to reveal static information.

The big type-theoretic idea here is "existential types" that packs data and not reveal information until it is unpacked.

Hope that was helpful. That was a great great question.

mathetic

hace 5 añosdiscuss

The goal is the same but the approach is different. This is entirely compile time and it covers all executions of the program, whereas taint analysis done at runtime and consider only some executions.

Also taint analysis typically doesn't track implicit flows described in the post, but detects the explicit ones.

mathetic

hace 5 añosdiscuss

The language is just assignment to simple variables (like `=` in C), sequencing (like `;` in C), if-then-else statements, and while loops.

The simple version uses algebraic data types (present in Rust, Haskell, OCaml to name a few) to describe the abstract syntax tree of the language.

The inference rules [0] (the bits that have lots of dashes in them) are standard notation for describing logic and type systems.

The rest of the post uses more advanced types, particularly generalised algebraic data types [1] which allow you to have interesting types that reveal information to the typechecker when you pattern match on them.

If you really want to get into type systems and programming language theory, Types and Programming Languages [2] is a classic.

If you just want to understand the privacy ideas, I describe what the rules are supposed to do in detail, so you can gloss over the actual syntax. The only thing that part adds is that I can make Haskell's typechecker prevent construction of privacy violating programs.

If anything is still unclear, feel free to reach out. I'm happy to explain and elaborate.

[0] https://en.wikipedia.org/wiki/Rule_of_inference

[1] https://en.wikipedia.org/wiki/Generalized_algebraic_data_typ...

[2] https://www.cis.upenn.edu/~bcpierce/tapl/

mathetic

hace 5 añosdiscuss

Let's say we have `a, b, d : 0` and `c : 999`. Then `a := b :>> c := d` according to your rule is well-typed and has a security level `999`.

Now let's say I have a conditional expression `private : 999`.

The following program typechecks according to the rest of the restrictions. In particular, `999` from `private` is less than or equal to the `999` from the sequenced command.

  ITE private $
    a := b :>>
    c := d

But we just leaked data because if the value of `a` (which we can observe) is not `b`, then we know that `private` was 0 (aka. false). This should never happen because `a` is public and `private` is private.

The intuition here is that the lower the security level a command has the more public the conditional has to be. Otherwise, private data would *influence* public data which we can then observe to deduce something about the private data.

> it seems like you could leak info by just assigning two variables, where one is always public.

I didn't quite follow this bit. But if you elaborate, I'm happy to discuss.

mathetic

hace 5 añosdiscuss

My bad, sorry =)

The share from this story is that we can enforce privacy just as we enforce more traditional types at no runtime cost. It scales because it is compositional and compiler can guide us through programs that won't leak data.

A more niche outcome is that Haskell's traditional type system is rich enough to encode this privacy enforcing type system.

I think if you just ignore the syntax, you can still gain a good intuition about how data might leak in subtle ways and what is sufficient to prevent it.

mathetic

hace 5 añosdiscuss

That is a different notion of typing. The type systems you are referring to (which is how they are commonly understood) classify data according to the operations they support. In this post, types classify privacy. These two notions are orthogonal and can be combined if needed. There are many many more notions of typing out there achieving wildly different goals.

mathetic

hace 5 añosdiscuss

Wouldn't that require the programmer to be adversarial?

Since all type systems have escape hatches, I don't think they would be resilient at all in adversarial settings. This is more geared towards detecting accidental and _subtle_ data leakage.

Submissions

Goto Assignment: A better local Goto Definition

The Lessons of the Pandemic (1919) [pdf]

comments