mathetic

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

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.

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.

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/

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.

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.

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.

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.

The point is often you don't need to. If you use Google docs, the chances are you will be editing it disjointly most of the time and occasionally you'll edit the same bit of the document. Then you don't really care if what comes out is a meaningful sentence, but that all parties involved (regardless in which order they see the operations) see the same version of the document so that they can fix it. That's what CRDTs buy you.

Without them, you have to use either explicit synchronisation which is a bad idea if you want local-first software (doesn't work offline, needs to be done even when editing disjoint bits of the file, etc.) or something like CRDTs. Now there is a great paper by Victor Gomes, Martin Kleppmann, and Dominic Mulligan that proves (in a proof assistant!) that pretty much all other alternatives that do not use strong consistency is flawed in edge cases.

As for triviality of the operations, I know for a fact that Martin Kleppmann has a paper in the works that show (and prove) how to do tree move efficiently as a CRDT. That means you can basically do arbitrary edits on JSON. Hopefully, that should clear up any confusion about for which applications it might be useful.

So I use QuickCheck often and I'm a true believer, but the point this post is making is absolutely justified. Tying the test generation to the type is often requires some creative ways of writing `Arbitrary` instances (the specification of how test cases should be generated).

However, I don't think what the author is suggesting in its place better. The advantage of tying the test case generation to the type is that it's compositional. Lots of sub Arbitrary instances come together to generate the test case and in the long term I find this to be more maintainable. Whereas the author's approach discourages compositionally.

The real problem is that the types in vanilla Haskell are too loose, so there lots of inhabitants of a type that we are not interested in. The author mentions in passing, dependent-types might be a solution and that is exactly right. What is needed is to make the irrelevant terms illegal altogether. This is pretty achievable and is already somewhat used. For example, the program synthesis (proof search) mechanism of Idris 2[0] uses linear[1] dependent types[2] to heavily constrain which terms are possible candidates for a given type. The specificity of the type reduces the search space, hence increases the effectiveness of the proof search.

[0] https://github.com/edwinb/Idris2

[1] https://en.wikipedia.org/wiki/Substructural_type_system#Line...

[2] https://en.wikipedia.org/wiki/Dependent_type

That doesn't help at all because although Datalog is a syntactic fragment, its dynamic semantics are very different, so the operations defined in Prolog standard are suggestive at best and completely nonsensical at worst.

For example, the program `p(X) :- p(X)` with query `?- p(X)` is an infinite loop in Prolog but in Datalog it terminates trivially and is equal to the empty set of facts for `p` in the absence any other facts.

I think it's more cultural than anything else. SQL, despite being declarative itself, has a more imperative feel to it for some people (recursion being at the fringes of its standard) and people seem to believe more declarative means slower and more difficult to comprehend. The former is true only due to the implementation effort that went into SQL engines and the latter is plain false.

It probably doesn't help that the standard presentation of Datalog looks very much like Prolog, which most people think is an esoteric and failed programming language.

As for its limitations, it's disciplined in a number of ways, but those are features rather than shortcomings. So you can see in the post that it employs syntactic restrictions to ensure domain independence, it doesn't allow function symbols to have termination. It requires predicates that are not purely logical (extralogical) to satisfy certain conditions for safe execution. These make sure that your queries are well-behaved even before you start running the query. There is research on relaxing these restrictions (cough my work cough) without compromising on the nice properties that come along with it.

The nice thing is of course that if you want to do the same for SQL you start with pandora's box open and try to contain the chaos inside again, while with Datalog you're carefully trying to make the best out of it without unleashing madness. The latter is a much nicer foundation.

OP here. Happy to answer any questions.

That's not always an option. Your career very much depends on consistently publishing in "A" venues (conference/journal). So it depends on your subcommunity's opinion on open access. For example, programming language people as a community are super keen on it, so most top venues are becoming open access. If that's not the case for your field, it's basically academic suicide unless you already have an amazing reputation.

It is a breath of fresh air seeing someone, after earning some success and wealth, still remembers the values he started out with.

Going a step further and being a good leader would I suppose be to steer the technology towards a tool that can create the values he desires e.g. advocate for proof of work that folds proteins.

Yes, I was thinking total with respect to _intuitive_ arguments, but wrote injective. Sorry.

Ah, that's a problem with many facets.

It is not that we can't come up with a logic language that is more declarative, it is just that telling the program everything about the universe is so damn dull. For example, ordering of your body predicates will often be based on what you think intuitively their sizes of solutions are going to be e.g. `plus(A,B,C), solution(C,X).` You know that plus is injective, so you put it first but from a logical perspective putting solution predicate first is just as sensible. If the language allowed you to express relative sizes of the predicates, then this could have been done automatically, but it would involve coding the order of predicates somewhere else in the program!

You also need to get rid of cuts in Prolog, if you want to be closer to true declarative programming. You might like to then try Datalog (alas, not Turing complete).

Another approach is to separate concerns more clearly. The part of Prolog that encodes and solves a logical problem is often different than the one dealing with IO for example. Ideally, you want to be more declarative in the former domain and more imperative in the latter. This can (and probably have been done) with a monadic approach.

Sure. Which subjects are you interested in?

I'm a grad student and I spend a lot of my time reading CS papers.

It is amazing that you want to start reading CS papers and I highly encourage it. However, if you don't have a CS degree I think papers might be remarkably off-putting (they usually are even to early grad students). I suggest you start with textbooks instead. Papers suffer from not being rewritten once they are published, hence from a pedagogical point of view, they are usually not explained as well as they could be after digesting them for many many years. Another problem is that most papers contain multiple ideas some of which rise and shine and the other ones die (often for good reasons). It is not easy to spot which is which without knowing about the wider context, which you naturally lack as a beginner.

If you insist on reading papers, however, at least don't read them in linear order. A good section order is abstract -> intro -> conclusion -> related work (because it uses comparisons which help) -> background -> evaluation (if exists!) -> technical chapters (those are usually best read in linear order). If there are proofs read them only if you must! If the proof is presented in the paper that is a good indication that it contains multiple subtle points which are tough to understand even if you are an experienced researcher.

We got caught up doing science of it all.

Nope. Strange loops are not by definition not intentionally circular (while a circular graph in a file system is in this case). He makes that clear I think in the final chapter of GEB.

He likes computers, he even likes AI. He doesn't buy into Ray Kurzweil's ideas about singularity [0,1]. He also (as I understand) is in Chomsky school of statistical learning as opposed to Peter Norvig (or Google) school [1,2]. Those two are highly unpopular stances to have these days, so I can see how that can be confused with not liking computers/AI.

If you read GEB, you can see in different chapters that he is a big fan of computers, simulations, attempts at AI, and the such.

[0] https://www.youtube.com/watch?v=Nhj6fDDnckE

[1] http://www.americanscientist.org/bookshelf/pub/douglas-r-hof...

[2] http://norvig.com/chomsky.html

The contrapositive is "if war doesn't start, trade doesn't stop."

For the love of God, cite something credible.

Well, that is a nasty thing to say, but my whole point was that a single person's reduced consumption doesn't help as much in the grand scheme of things just because of exponential growth.

Well, I constrained the scope, but CO2 emission is not the only problem about the environment. Most resource are scarce and although I believe in Elon Musk as much as the next techie, we can't just take a leap of faith. Water is scarce, energy is scarce (though we are getting better), but we are growing at an unsustainable rate.

Now the main problem is that if you reduce your CO2 emission by 80% and you and all your offsprings have two kids and each consume at your reduced level, in just two generations, it would been better if you didn't have kids. Two generations after that even at the reduced consumption, you (by having kids) contribute to CO2 emission by a factor of 6 if you have just consumed all the meat and didn't have kids.

Geometric progression is a nasty nasty thing.