3L Security

First Class Environments

The 3L Project

Scheme based Operating System

3lproject.org

• Secure
• Extensible

Modes

• Development
• Secure (this talk)

Note:

• High level
• Simplified
• WIP

Scheme (R7RS) compatibility

• Extension of Scheme, not itself portable
• Potentially portable but SLOW
• R7RS programs work without modification

Environment

Collection of visible bindings

> (define foo 1)
> foo
1 ; foo is in the environment
> bar
error - bar not bound ; bar not in the environment

Example

> (define foo 10)
; undefined
> foo
10
> (eval 'foo (interaction-environment))
10
> (with-environment (interaction-environment)
    foo))
10
> (with-environment (make-environment (empty-environment))
    foo)
error - foo undefined

Same foo

> (define foo 10)
; undefined
> foo
10
> (eval 'foo (interaction-environment))
10
> (with-environment (interaction-environment)
    foo))
10
> (with-environment (make-environment (empty-environment))
    foo)
error - foo undefined

Same foo

> (define foo 10)
; undefined
> foo
10
> (eval 'foo (interaction-environment))
10
> (with-environment (interaction-environment)
    foo))
10
> (with-environment (make-environment (empty-environment))
    foo)
error - foo undefined

Same foo

> (define foo 10)
; undefined
> foo
10
> (eval 'foo (interaction-environment))
10
> (with-environment (interaction-environment)
    foo))
10
> (with-environment (make-environment (empty-environment))
    foo)
error - foo undefined

Same foo

> (define foo 10)
; undefined
> foo
10
> (eval 'foo (interaction-environment))
10
> (with-environment (interaction-environment)
    foo))
10
> (with-environment (make-environment (empty-environment))
    foo)
error - foo undefined

New environment - foo unbound

> (define foo 10)
; undefined
> foo
10
> (eval 'foo (interaction-environment))
10
> (with-environment (interaction-environment)
    foo))
10
> (with-environment (make-environment (empty-environment))
    foo)
error - foo undefined

Security through environments

> (with-input-from-file "passwords"
     (lambda () (read)))
all my passwords
> (print-file "untrusted-file-from-internets.scm")
_(define (run)
  _(with-input-from-file "passwords"
      (lambda () (read))))
> (with-environment/files (no-i/o-environment)
      '("untrusted-file-from-internets.scm")
    (run))
error - with-input-from-file not defined

interaction-env can read files

> (with-input-from-file "passwords"
     (lambda () (read)))
all my passwords
> (print-file "untrusted-file-from-internets.scm")
_(define (run)
  _(with-input-from-file "passwords"
      (lambda () (read))))
> (with-environment/files (no-i/o-environment)
      '("untrusted-file-from-internets.scm")
    (run))
error - with-input-from-file not defined

Untrusted internet program

> (with-input-from-file "passwords"
     (lambda () (read)))
all my passwords
> (print-file "untrusted-file-from-internets.scm")
_(define (run)
  _(with-input-from-file "passwords"
      (lambda () (read))))
> (with-environment/files (no-i/o-environment)
      '("untrusted-file-from-internets.scm")
    (run))
error - with-input-from-file not defined

error - no i/o bindings

> (with-input-from-file "passwords"
     (lambda () (read)))
all my passwords
> (print-file "untrusted-file-from-internets.scm")
_(define (run)
  _(with-input-from-file "passwords"
      (lambda () (read))))
> (with-environment/files (no-i/o-environment)
      '("untrusted-file-from-internets.scm")
    (run))
error - with-input-from-file not defined

Create environments

> (define (no-i/o-environment)
    (make-environment (empty-environment) (import (scheme base))))

Restricted imports

Code can only import packages it's environment has a reference to

i.e. no-i/o-environment can't import (scheme files) to get file i/o

Environments

• Objects
  • Created
  • Referenced
  • Inherited
  • Bound
  • Queried
  • Modified

3L Project + references

3lproject.org

References (partial list):

• Ron Garret - Lexicons, Locals
• Robert Strandh - First-class Global Environments in Common Lisp
• Jonathan A. Rees - A Security Kernel Based on the Lambda Calculus