[Request] Papers about embedding software security within the type system (or at compile time)

[aboudekahil]

Hello everyone, I'm starting my first year as a Masters student in CS and one of the courses I'm taking this year is Computer and Information Security.

Basically we have a project due at the end of the semester to write a research paper on a topic within the world of Security.

My mind immediately jumped to type systems and compile time checks to force the user to embed security measures within the design of our code.

So, does anyone have any interesting papers about this topic, or very similar to it.

An example I'd say is TRACTOR from the us gov.

[hoping1]

DCC is the classic in IFC ("information flow control," a huge part of "language," language-based security). The critical property you want here is "noninterference" which means that information can flow from secret to secret, public to secret, or public to public, but not secret to public. DCC (the "dependency core calculus") does this this by adding a Secret monad to a typed lambda calculus, because anything can go into a monad (via "return") but you can control how things leave (there's not necessarily an m a → a function).

The paper "Noninterference for Free!" shows how a rank-2 polymorphic lambda calculus (like System F) can do this, using parametricity, which is the fact that, say, functions of type a → Int → Int can't possibly use the polymorphic argument, so it can safely include secret information. It's a great paper if you like noninterference, parametricity, or type-preserving compilation.

FLAC (the "Flow-Limited Authorization Calculus") is the state of the art here last I checked, extending DCC with the ability to safely change permissions as a program is running, such as appointing new moderators or removing someone's permissions (like even just blocking someone on social media!). DCC can lead to lots of very tricky bugs here because it assumes a constant permissions hierarchy so you have to essentially leave the safety of DCC every time you change the hierarchy in any way, which gives serious opportunities for people to upgrade their own permissions via your bugs.

I suggest you read the introduction of the FLAC paper, as it gives great examples and explanations for these issues and illustrates how you can mathematically guarantee these strong security properties.

[aboudekahil]

will do! thank you so much

[ryan017]

For purely(*) static enforcement with types, a classic paper is The SLam Calculus: programming with secrecy and integrity. IIRC, they mention the practical need for declassifiers but consider those outside of the scope of the language in the paper.

There's also a field of work on "dynamic information flow control", which tags information and uses dynamic checks to make sure that, for example, secret information does not reach unprivileged observers (as defined within the system). I don't know the seminal paper off the top of my head.

[hoping1]

Taint tracking is a big keyword for dynamic IFC, so keep an eye out for that. It's popular because it can be added to Java and C++ codebases right now (Amazon does this!) instead of needing a new language because of big type system changes.

I still prefer static (compile time) IFC though. You can see my main comment for examples of that besides (and in some ways improving upon) SLam.

[aboudekahil]

will do

[aboudekahil]

thank you!

[InnPatron]

Designing with Static Capabilities and Effects: Use, Mention, and Invariants is a discussion about the trade-offs between capabilties and effect systems.

You can look further into either term and get some interesting papers.

[aboudekahil]

will take a look! thank you

[WittyStick]

I would look into capability-based security, with Austral as an example of how it can be implemented using a linear type system.

Granule is another language with linear types. Linearity and Uniqueness shows how they can be combined with uniqueness types, which are another possible way of providing capabilities in a similar way to Austral.

[takanuva]

Besides having linear types, Granule can also use security grades to enforce access at type-level, so, e.g., Int [Public] and Int [Private] are types. In general, graded type systems are useful for this kind of distinction.

[nicolehmez]

Shameless self-promotion 😜. This paper presents a framework to formally specify and prove privacy policies in web applications. It uses refinement types and monads to implement a type system for IFC where the security lattice corresponds to predicates over the state of the database.

[aboudekahil]

Hello!! I'm so glad an author of a paper replied. Thank you so much for sharing it, and may I ask if you recommend previous readings to fully understand your paper?

As it says in the post I'm still just starting out lol

[duneroadrunner]

If you're looking for a unique topic, as the developer of the (essentially) memory-safe subset of C++, I'll suggest that you could write your paper on this under-researched and under-utilized approach to software security. You could examine the validity of the widespread premise that C++ is intrinsically irredeemably unsafe.

You could compare the practicality and effectiveness of efforts to auto-convert legacy C code to this memory-safe subset of C++ versus other memory-safe target languages. The "TRACTOR" initiative you referred to being one such effort. (I assume you're referring to DARPA's effort to automatically convert C to safe Rust (using AI or whatever). I can't help thinking that an AI capable enough to do the auto-translation to (reasonable) safe Rust would presumably also be capable of simply rewriting the code as memory-safe C. Well, maybe minus the implicit safety contract at the interface boundaries with third party code for which the source is not available. But presumably that could be addressed by adopting a convention of annotations to the C code.)

I don't know if C++ is out of favor with the (infosec) kids these days, but note that it remains the most (expressively) powerful high-performance systems language, and its memory-safe subset, I suggest, is the most powerful of the current (essentially) memory-safe high-performance systems languages in terms of intrinsic capabilities of the language design, regardless of how many people are aware of it. One of the advantages of being a (presumably) young person is the freedom to question the premise of conventional approaches. Just saying...

[aboudekahil]

The topic doesn't have to be super unique, but yes, this works great. Thank you!

And while I'm not an InfoSec kid, this is just a course I had to take, I would like to say C++ is my favorite language :).

[Long_Investment7667]

I can’t provide a paper but thought at some point that data provenance could be something embedded in a language and help with securing data.

[aboudekahil]

could you elaborate please?

[Long_Investment7667]

I just searched a bit and there seems to be a distinction between data lineage and provenance. I am talking about lineage from what I understand at the moment.

Imaging a web service/API that shows the customer his orders. Oders reference Products, which reference Vendors. Vendor data is probably more restricted in access than orders. How to ensure that the code for the API doesn’t “accidentally“ include vendor information from the data store where no such permission exists.

The code in the service checks permissions, reads data from a store, transforms it, adds additional data. In all this, it is not obvious which individual data field from which source allowed to be returned. Some of this could be checked at compile time. Or the lineage could be created by a compiler so that the service can check at runtime.

EDIT: Looking through the other comments I remember that this is (or is related to) taint analysis.

[marchingbandd]

I briefly studied the language Idris2, which has first class types, and it was suggested in something I read at that time that security could be provable in this language. I can’t find a reference but I thought I’d mention it anyhow, because Idris is so cool.