Building "#lang dungeon"

[Christopher Lemmer Webber]

Every day the threats facing our computing environments are getting
worse. Recent incidents in both gems and npm have shown modules
exfiltrating information from developers' machines or production
servers. It is likely that soon package managers will also be targeted
to install cryptolockers to attack developers' machines, or worse,
install backdoors that allow an attacker to perform arbitrary execution.
How can we make Racket not only a fun and fulfilling development, but
also a safe one?

Thankfully, Jonathan Rees did the kind work of laying out the recipe for
dramatically improved safety over two decades ago:

http://mumble.net/~jar/pubs/secureos/secureos.html

It turns out that the lambda calculus already provides the fundamental
layer of security we need; code can only perform actions it has
references to. This is called "object capability (ocap) security";
a decent (ok, I'm biased) intro to the ideas can be found on this
podcast episode if you are interested:

https://librelounge.org/episodes/episode-13-object-capabilities-with-kate-sills.html

Racket already has most of the pieces in place; we just need to add one
more thing. Consider and contrast the following scenarios:

Conventional Racket scenario:

;; Runs a game of solitaire.
;; Also has access to your entire filesystem, can secretly exfiltrate
;; data or install backdoors, etc etc.
(solitaire)

A more desirable scenario:

;; Runs a game of solitaire.
;; *Only* has access to a stream of input when the window is active,
;; the ability to draw to a *specific* window on the screen, the
;; ability to read/write from a single file on disk, the save file.
(solitaire get-input
display-graphics-to-window
save-file-access)

Now the amount of damage that solitiare can perform is significantly
curtailed. It can perhaps display images we would not like to see
or write nonsense to its save file, but it cannot do anything else.
(We could also put limits in the save-file-access procedure on how
large of a file it is allowed to write, if we were worried about that.)

The key idea here is that authority flows through the system the same
way that data naturally flows through a program. You simply don't have
more access than what you allowed to flow through.

So what is necessary to make Racket ocap-secure? The primary problem is
the assumption of "require", that any module can "reach out" and gain
access to anything it likes, be it network access or file access or etc.

What I would like instead is to allow modules to be "granted" access.
The idea is in fact the same as with the solitaire-as-procedure solution
above: modules gain access not by reaching out and grabbing whatever
they want, but by being "handed" access. Imagine your module as one big
procedure where we pass in access to other modules/values/macros and
you'll get the idea.



#+BEGIN_SRC racket
#lang dungeon

; passed in, already fully "empowered"
(require match
graphics-tools
keyboard-tools
;; the parent module must trust us a lot, they gave us full
;; filesystem access!
general-file-io
;; solitaire needs picture constructors to generate graphics
(empower solitaire graphics-tools))

(provide run-solitaire)

(define (get-input input-source)
...)

(define (display-graphics-to-window ...)
...)

(define (make-save-file-access filename)
(match-lambda
[(list 'read) (call-with-input-file filename port->bytes)]
[(list 'write bytes)
(call-with-output-file filename
(lambda (p)
(write-bytes bytes p))
#:exists 'replace)]))


(define (run-solitaire [save-file "~/.racket-solitaire"])
(solitaire get-input display-graphics-to-window
(make-save-file-access save-file)))
#+END_SRC

I've handwaved over a couple of things, but this module shouldn't be
afraid that the solitaire procedure that comes from the empowered
solitaire module has access to dangerous things such as the full
filesystem (even though the importer of *this* module trusted it to have
full filesystem access), and neither module has network access.

I don't know how to build this fully; I know that:
- we need code inspectors to prevent evil hygeine-breaking, but good
news we have that
- I need a way to make *something like require* work, but where the
import-er is able to very explicitly pass in which modules are
allowed. This seems to mean something *like* controlling the module
registry. Note that this also means that the names of the modules
being imported aren't from a "global registry" anymore, it's the
names that the empowering-module provided.

There's an alternative, which is the emaker / frozen realms approach.
This approach actually instead gives you an extremely minimal base
syntax that *cannot be extended*. No new macros. Instead, the module
that is imported wakes up in a cold world of just a few primitives... no
mutable state, very few authenticated things, etc. The module then
returns a function that does the interesting things: we can pass in
arguments to get out the "interesting" things that the module can
provide. You are mostly left with the cold world of lambda and a few
carefully chosen macros.

But that's kind of sad to throw away macros, imo. I'm not sure the
racket community will be happy enough to use it. I'm not sure I would
be.

So, how to build this? It doesn't seem that there's a way to control
the module registry being used in a require-ing context. But maybe
there's something else.

Thoughts, or solutions, welcome.
- Chris

[Dionna Amalie Glaze]

Capabilities can be tracked with continuation marks. For a language to grant a subset of capabilities to a required module, you can do something like contract-in that will wrap identifiers with a with-continuation-marks capability restriction. The tricky part becomes how to make all I/O subsystems etc. actually consult and respect the capabilities that are marked on the continuation. That will take a really invasive change to the runtime, or a flawed approach of a wrapper language around #%kernel such that everything that builds on top of it respects capabilities. Unfortunately we can't treat existing modules like functors for which we can replace the underlying #%kernel.

--
You received this message because you are subscribed to the Google Groups "Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/87y310r3b1.fsf%40dustycloud.org.
For more options, visit https://groups.google.com/d/optout.

--

-Dionna Glaze, PhD (she/her)

[Christopher Lemmer Webber]

Hi Dionna, thanks for your reply!

I gave a response to you IRL that I think I hadn't conveyed here which
is that there's a reason I'm taking the lambda-approach to capabilities
(which is explicit) vs an ambient/dynamic approach of continuation
marks. One reason is that the work I'm trying to build can have
references that cross machines (Goblin[oid] has preliminary support for
this, but it isn't really fully implemented yet); in order for those to
work, we can't rely on runtime scope behavior since we also are going to
compose with remote capabilities as well, which do not have access to
our inner runtime.

I hear your concern that this is too much explicit argument passing; the
only thing I suppose I can respond with is that this is how previous
ocap systems have worked. One thing that helps a lot is that we can
compose capabilities by enclosing over them, and often times doing this
enclosure can abstract the necessary things we need, but it does indeed
result in more argument passing.

[ra...@airmail.cc]

There is http://shill.seas.harvard.edu/ it runs on freebsd.

[Christopher Lemmer Webber]

ra...@airmail.cc writes:

> There is http://shill.seas.harvard.edu/ it runs on freebsd.

Yes, it's a good source of inspiration. However it's really meant for
shell scripting and isn't quite a good fit for the case I need, which is
for more general racket programming.

[Konrad Hinsen]

Hi Chris,

While I understand the general goal you are aiming at, it isn't quite
clear to me who you are trying to protect against who. There's a wide
spectrum of people involved, ranging from language designers via library
developers and application developers to end users. Who is going to
define your capabilities? Who is supposed to be protected by them? And
who is the potential villain whose evil doings need to be checked for?

Your example doesn't help much with this, as playing a game of solitaire
from the Racket REPL is not a relevant real-life scenario. The typical
solitaire player is an end-user who double-clicks an application and
wouldn't understand the implications of granting access to a single
window. Technical measures to establishing trust work only between
technology experts. So perhaps you aim at protecting application
developers against abusive libraries? In that case, I'd expect the main
challenge to be the design of a sufficiently flexible yet manageable
capability system that doesn't add tons of additional complexity to
software.

Konrad.

[Christopher Lemmer Webber]

Konrad Hinsen writes:

> Hi Chris,
>

Hi Konrad,

> While I understand the general goal you are aiming at, it isn't quite
> clear to me who you are trying to protect against who. There's a wide
> spectrum of people involved, ranging from language designers via library
> developers and application developers to end users. Who is going to
> define your capabilities? Who is supposed to be protected by them? And
> who is the potential villain whose evil doings need to be checked for?
>
> Your example doesn't help much with this, as playing a game of solitaire
> from the Racket REPL is not a relevant real-life scenario. The typical
> solitaire player is an end-user who double-clicks an application and
> wouldn't understand the implications of granting access to a single
> window.

Of course I don't expect someone to launch solitaire from the REPL, and
indeed there are UX considerations once we move from the REPL to actual
program launch. There *are* paradigms for that that have been
developed, and intuitive behaviors such as drag and drop compose nicely
with a capability discipline.

However, I am talking to language people about how we give authority to
parts of our programs, so something that works at the REPL can help us
think more at this level of abstraction, aside from the other ones :)

[Konrad Hinsen]

Hi Christopherm

> Of course I don't expect someone to launch solitaire from the REPL, and
> indeed there are UX considerations once we move from the REPL to actual

I wasn't thinking so much of UX issues, but of the differences in the
level of abstraction that different people need. The capabilities that
you would pass to a low-level file handling library may well make no
sense to the end user who is barely aware that his solitaire game
uses files to store scores or whatever else.

Android permissions are a good illustration. They are too coarse-grained
for meaningful protection (e.g. access to the whole filesystem or no
files at all), and at the same time too technical for most users who
don't know (nor want to know) how and where data is stored.

Konrad.

[Neil Van Dyke]

If you want to solve problems like how to handle user conceptual models
of permissions, consider putting "UX" aside for a moment.

UX gets confused by conflicts of interest, which the earlier disciplines
of HCI and human factors engineering did not much have.

HCI comes from a human factors tradition of goal alignment with the
human -- everyone wanting the user to be more effective at their tasks
(whether it's operating a Macintosh, or a fighter jet).

UX is influenced more by the traditions of graphic design (especially
for marketing brochures and the like), and in practice is usually
burdened by motivations to manipulate the user to serve the interests of
someone other than the user, even aggressively against the interests of
the user.

Consider the GUI design for a smartphone/tablet -- do you want its
visual cues, notifications, and other affordances to be for effective
use of the device (HCI), or do you want to combat users' ability to
perceptually filter-out ads, use notifications to aggressively keep the
user engaged with addictive low-value "content", us more-blatant "dark
patterns" to discourage users from selecting options that are likely the
user's intent and in user's best interest, while looking slick (UX).

So, as an engineer/scientist/designer/educator of goodwill, consider the
exercise of trying to think like an HCI person, and being suspicious of
anything labeled UX.

[Philip McGrath]

I wonder if the unit system, or something like it, could be a basis for implementing this, especially the aspect of avoiding too much explicit argument passing.

Signatures can define bundles of identifiers, like file IO primitives. This lets you avoid having to know which specific primitives are being used, as long as they're collected in groups with the same security implications (e.g. `call-with-input-file` and `open-input-file` are probably equivalent). The untrusted `#lang dungeon` module could see the specifications for these identifiers without having access to the values/implementations: it would define and provide a unit importing (in the `racket/unit` sense) the signatures for the capabilities it needs. The more-trusted module invoking the `#lang dungeon` unit would have to link it with a unit supplying the needed capabilities, either from the root environment or by importing those capabilities (or stronger ones) in itself. The unit system also supports things like deriving restricted versions of a signature's values that obey the same specification.

Probably you would want to build some scaffolding over `racket/unit` specific to ocap security, and a caveat in all of this is that my understanding of ocap security isn't especially deep. But what you describe sounds like dynamic linking, which is what units are designed for. I would start by looking in that direction before trying to interpose on the module registry: modules are basically designed for first-order, static linking.

-Philip

--
You received this message because you are subscribed to the Google Groups "Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/87r26sqp8x.fsf%40dustycloud.org.