Writing secure applications in Scheme

[ posted to comp.lang.scheme ]
http://groups.google.com/groups?selm=xcgpth3eify.fsf%40mccarthy.emba.uvm.edu

Win Treese wrote:
> I was intentionally vague so as to cast a wide net, but I'll be more
> specific. I'm interested in the engineering techniques for avoiding
> security problems in application code. In C, for example, the number
> one problem (of course) is buffer overflows, and one can find coding
> guidelines (indeed, entire books) that talk about how to avoid such
> problems.
>
> In the Common Lisp world, a good example is to use:
>
>    (setf *read-eval* nil)
>
> so that the reader doesn't help do bad things to you. Another example
> is how to be careful with eval.
>
> But another aspect is a broad survey of security with respect to
> Scheme, including mobile code, interfaces and subsystems for
> cryptography, etc. And anything I've missed.

Hello Win,

The need for programming language based security is apparent.  The President's
Information Technology Advisory Committee's 1999 report "Information
Technology Research: Investing in Our Future" [1] makes the case quite clear.
The report states, "technologies to build reliable and secure software are
inadequate."

   Large software systems are beyond our capability to describe
   precisely. Consequently, there is little automation of their construction,
   little re-use of previously developed components, virtually no ability to
   perform accurate engineering analyses, and no way to know the extent to
   which a large software system has been tested.

   Having meaningful and standardized behavioral specifications would make it
   feasible to determine the properties of a software system and enable more
   thorough and less costly testing. Unfortunately such specifications are
   rarely used. Even less frequently is there a correspondence between a
   specification and the software itself. Often software behavior and flaws
   are observable only when the program is run, and even then may be invisible
   except under certain unusual conditions. Programs written in such
   circumstances frustrate attempts to create robust systems and are
   inherently fragile.

   Software development relies on individual genius and creativity, and, as
   with all design-based disciplines, will continue to do so. But it has
   become clear that the processes of developing, testing, and maintaining
   software must change.  We need scientifically sound approaches to software
   development that will enable meaningful and practical testing for
   consistency of specifications and implementations. This requires long-term
   research in languages, theories, simulation, analysis, and testing that
   could lead to standardized multilevel mechanisms similar to those which
   have created the success in computer-aided design for digital hardware.

There have been significant advancements in "scientifically sound approaches
to software development" with respect to security, but there is much left to
do, including the widespread adoption of such disciplines into everyday
software development.  Part of the problem is that scientifically sound
approaches to software development *in general* have not yet received their
due credit and adoption into mainstream development practices and programming
languages.  For example, language-based security is predicated on language
safety, that is programs behave only in a well-defined and consistent manner.
Scheme, ML and Java are examples of safe languages (many others exist) and
there are even safe dialects of C such as Cyclone [2].  You mention the buffer
overflow problem endemic to C programs.  A study of the alerts issued by the
Computer Emergency Response Team (CERT) concluded that around 50% are caused
in part by buffer overflows and yet this problem has been solved by safe
languages for decades!

Ok, so let's look at some of these approaches.

The (setf *read-eval* nil) example you give is what I would call a
namespace-based capability model; potentially dangerous operations cannot be
named and therefore used by untrusted code.  There's an interesting thread on
the PLT mailing list, "Scheme interpreter with web interface ?" [3], which
became "Security models in mzscheme ??" [4] about executing mobile, untrusted
Scheme code in a sandbox environment.  Paul Graunke talks about the namespace
aspect of such an endeavor.

Namespace-based capability security is intimately related to the object
confinement problem.  Object confinement is concerned with the encapsulation
or protection of object references.  If our language provides some kind of
code boundary mechanism like a module system, then we want to restrict
sensitive references to certain trusted boundaries or domains.  An object
confinement system should provide a means of specification and enforcement of
reference flows among domains.  Skalka and Smith have done work in this area
by developing type-based approaches to static enforcement of object
confinement [5] and Borris Bokowski and Jan Vitek [6] have proposed extensions
to add a notion of "confined types for Java as an aid for writing secure
code."

   One way of thinking about confined types is as a machine checkable
   programming discipline that prevents leaks of sensitive object
   references. [...] [W]e are suggesting guidelines how to use Java's existing
   facilities to enforce the desired encapsulation property.  Given some
   definition of a protection domain, we say that a type is confined to that
   domain if all references to objects of that type originate from within the
   domain.  In other words, code outside of the domain should never be allowed
   to manipulate confined objects directly.  Confinement differs from existing
   access control mechanisms in that it constrains access to object references
   rather than classes. The difference is most visible when considering
   subtyping.  Class-based restrictions (such as the Java private keyword) can
   be circumvented by casting the protected object to one of its unrestricted
   supertypes.  With confined types this is not allowed. For all practical
   purposes, confined types should be viewed as enforcing static scoping on
   dynamic object references.

To see an example of where a confinement system would prevent a security
breach consider the following:

   In Java, each class object --that is each instance of class Class-- has a
   list of signers. These signers are principals under whose authority the
   class acts. This list is used by the security architecture to determine
   access rights of the class at run-time.  A leak of a reference to this
   internal data structure was the cause of a security flaw that allowed
   untrusted applets to gain all access rights in JDK 1.1.  The breach was
   caused by the conjunction of two seemingly innocuous operations.  The first
   operation is a method of java.security.IdentityScope which allows any
   applet to find out all the principals known to the system, amongst which
   some are likely to be trusted.  The second operation allows a class to get
   the list of principals that signed it.  The method that returned the array
   of signers erroneously returned an alias.  Arrays being mutable data
   structures, the applet then only needs to update the array with the
   signature of trusted principals to gain that principal's access rights."

In other words IdentityScope contained the following code (this bug was
discovered by the Princeton Secure Internet Programming group [7]):

   private Identity[] signers
   public  Identity[] getSigners(){ return signers; }

Which is obviously bad, but certainly "legal" Java code.  An object
confinement system could be used to prevent these types of security bugs.

Another approach to language-based security is discretionary access control.
An example of a rudimentary access control mechanisms is the UNIX file system.
For any given file, you have an access control matrix specifying who is
privileged to perform certain actions (rwx).  Access control in a programming
language specifies certain privileges that code originating from some location
or some author is capable of performing.  Your *read-eval* example could be
accomplished by denying the privilege to execute *read-eval* to any non-local
code.

Stack inspection is an enhancement of this technique that allows code of
various degree of trust and privilege to interact.  All or nothing security
mechanisms seem to be pretty easy to implement and use, but they are overly
restritive.  For example, Java's early sandbox model was an all or nothing
mechanism.  Applet code runs in a depleted environment lacking the ability to
perform any potentially malicious action, while local code runs with all
possible privileges.  Stack inspection allows us to enforce more fine-grained
policies in a disciplined manner.  Stack inspection primitives are now
implemented in the Java Virtual Machine and the Common Language Runtime,
although there are some differences between the two systems.  SI requires the
following primitives:

   enablePrivilege()
   disablePrivilege()
   checkPrivilege()
   revertPrivilege()

A description of stack inspection is given in [8]:

   When a dangerous resource R (such as the file system) needs to be
   protected, the system must be sure to call checkPrivilege(R) before
   accessing R.

   When code wishes to use R, it must first call enablePrivilege(R). This
   consults the local policy to see whether the principal of the caller is
   permitted to use R. If it is permitted, an enabled-privilege(R) annotation
   is made on the current stack frame. The code may then use R
   normally. Afterward, the code may call revertPrivilege(R) or
   disablePrivilege(R) to discard the annotation or it may simply return,
   causing the annotation to be discarded along with the stack
   frame. disablePrivilege() creates a stack annotation that can hide an
   earlier enabled privilege, whereas revertPrivilege() simply removes
   annotations from the current frame.
   ...
   The [checkPrivilege()] algorithm searches the frames on the caller's stack
   in sequence, from newest to oldest. The search terminates, allowing access,
   upon finding a stack frame that has an appropriate enabled-privilege
   annotation. The search also terminates, forbidding access (and throwing an
   exception), upon finding a stack frame that is either forbidden by the
   local policy from accessing the target or that has explicitly disabled its
   privileges.

The Java stack inspection algorithm looks like this:

checkPrivilege (target) {
  // loop, newest to oldest stack frame
  foreach stackFrame {
    if (local policy forbids access to target by class executing in
        stackFrame)
      throw ForbiddenException;

    if (stackFrame has enabled privilege for target)
    return; // allow access

    if (stackFrame has disabled privilege for target)
      throw ForbiddenException;
  }

  // if we reached here, we fell off the end of the stack
  // what to do in this case is an implementation decision

  // By default, deny access.
  // throw ForbiddenException;

  // Or
  return; // allow access
}

PLT recently added support for an access control mechanism [9]:

   To make sand-boxing easier, we've added an access check around each access
   of the filesystem or network in MzScheme's primitives. The access check
   calls a function provided by the current security guard --- as determined
   by the new `current-security-guard' parameter --- giving the guard a
   pathname/hostname, plus an indication of the kind of access that is needed
   (read, write, etc.). If the function does not raise an exception, access is
   granted.

   For example, evaluating the following expression should cut off all
   filesystem and network access:

    (current-security-guard
        (make-security-guard (current-security-guard)
            ;; filesystem check:
            (lambda (who path mode) (raise 'no-filesystem!))
            ;; network check:
            (lambda (who host port-number) (raise 'no-network!))))

   A new security guard can be created only as a child of an existing security
   guard, and access checks always consult the parent as well as the child, so
   a program can't arbitrarily increase its access by creating a new security
   guard.

A more Java-like stack inspection mechanism could be implemented using the
continuation-marks primitives provided with PLT Scheme.

Skalka and Smith [10] develop a static approach to stack inspection.  They
develop a lambda calculus extended with stack inspection primitives and a
security type system that provides the same guarantees as Java's stack
inspection.  These security types can be inferred and type safety implies
well-typed programs do not cause stack inspection failures, obviating the need
for run-time stack inspection.

Another approach to security is by information-flow analysis.  While access
control mechanisms are concerned with access to information, information flow
is concerned with it's propagation.  Heintze and Riecke [11] develop a lambda
calculus with an information-flow type system such that well-typed programs
exhibit what's called the noninterference property; an attacker cannot observe
any difference between two executions of a program that differ only in their
confidential input.  There is a compiler for Java that utilizes an
information-flow type system called JIF [11], and Sabelfeld and Myers recently
published an extensive survey on the topic, "Language-Based Information-Flow
Security" [12].

There are many other approaches to language based security that would be
amenable to implementation in Scheme such as cryptographic primitives, typed
assembly language, proof carrying code and certifying compilation.  At this
point though, I'm out of breathe.  I'll see if maybe some fellow foundations
of security summer school students can comment further.

Good luck on your presentation!

-d


 [1] http://www.ccic.gov/pitac/report/
 [2] http://www.research.att.com/projects/cyclone/
 [3] http://www.cs.utah.edu/plt/mailarch/plt-scheme-2000/msg00763.html
 [4] http://www.cs.utah.edu/plt/mailarch/plt-scheme-2000/msg00766.html
 [5] @InProceedings{skalka-smith-fcs02,
       author       = {Christian Skalka and Scott Smith},
       title        = {Static Use-Based Object Confinement},
       booktitle    = {Proceedings of the Foundations of Computer Security
                      Workshop (FCS'02)},
       month        = {July},
       year         = {2002},
       address      = {Copenhagen, Denmark},
       ps = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-smith-fcs02.ps}
     }
 [6] @Article{vitek-bokowski-spe01,
       author       = {Jan Vitek and Boris Bokowski},
       title        = {Confined Types in Java},
       journal      = {Software---Practice and Experience},
       year         = 2001,
       volume       = 31,
       number       = 6,
       pages        = {507-532},
       month        = {May}
     }
 [7] http://www.cs.princeton.edu/sip/news/april29.html
 [8] @InProceedings{wallach-felten-stack-98,
       author       = {Dan S. Wallach and Edward Felten},
       title        = {Understanding {Java} Stack Inspection},
       booktitle    = {Proceedings of the 1998 {IEEE} Symposium on Security
                      and Privacy},
       month        = may,
       year         = {1998},
       ps = {http://www.cs.princeton.edu/sip/pub/oakland98.ps.gz},
     }
 [9] http://www.cs.utah.edu/plt/mailarch/plt-scheme-2002/msg00481.html
[10] @InProceedings{skalka-smith-icfp00,
       author       = {Christian Skalka and Scott Smith},
       title        = {Static Enforcement of Security with Types},
       booktitle    = {Proceedings of the the Fifth {ACM} {SIGPLAN}
                      International Conference on Functional Programming
                      (ICFP'00)},
       month        = SEP,
       year         = {2000},
       pages        = {34--45},
       address      = {Montréal, Canada},
       ps = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-smith-icfp00.ps}
     }
[11] http://www.cs.cornell.edu/jif/
[12] @Article{sabelfeld-myers-jsac03,
       author       = {A. Sabelfeld and A. C. Myers},
       title        = {Language-Based Information-Flow Security},
       journal      = {IEEE J. Selected Areas in Communications},
       year         = 2003,
       month        = jan,
       volume       = 21,
       number       = 1,
       pages        = "5--19"
       ps           = {http://www.cs.cornell.edu/~andrei/jsac.ps}
    }