[e-lang] Notes from latest Joe-E meeting

[Mark Miller]

Forwarded by permission

---------- Forwarded message ----------
From: David Wagner
Date: Apr 24, 2007 5:35 PM
Subject: Re: Can we meet to discuss Joe-E this week?
To: Mark Miller, Adrian Mettler, David Wagner, Tyler Close, Marc
Stiegler, Ka-Ping Yee


Here are notes from our meeting today.


We all have to think about how to handle Errors due to
out-of-stack-memory conditions and the security holes associated
with try-finally, VirtualMachineExceptions, and JoeE.abort().

TODO:
- Check that primitive arrays are honorarily Equatable (they should be).
  Check that the spec states this.
- Change ConstArray and subclasses to avoid using Arrays.equals()
- Remember that taming database must prohibit use of Arrays.equals(),
  since it exposes == to callers even if the type of the elements are
  Selfless
- Change ConstArray.toArray() to pass in an array and use the runtime
  type of the array passed to that method, not the runtime type of the
  'arr' instance field of ConstArray.  i.e., the signature is
    public <T> T[] toArray(T[] result);
  After this change, ConstArray instances do not have any notion of an
  element type (statically, they have an alleged element type E, but
  clients cannot count on it being correct; dynamically, the implementation
  has an element types, but it isn't exposed, so clients cannot see any
  notion of an element type).
- Add parameter-less toArray() method to ByteArray, BooleanArray, etc.
- Deflection.allowed(): document that this is intended to allow you
  to dynamically invoke only the public subset of what Joe-E code can
  statically call.
- charset: Change "throw new UndeclaredThrowableException" to throw
  some kind of Error.
- charset.UTF8: Adrian might move the escape() and unescape() methods
  into a different class under charset.
- NoSuchMember should change to NoSuchMemberException
- Reflection: static fields "statics" and "instance" should be all-caps.
- Reflection: change name of field() to declaredField().
- Reflection will be changed: we get rid of field(), fields(), method(),
  methods(), constructor(), constructors(), and replace them with a thin
  wrapper around Class.{getField(), getMethod(), getFields(), getMethods()
  getConstructor(), getConstructors()} -- i.e., using a wrapper that is the
  minimum necessary for security.  The wrapper only needs to restrict to
  the publicly-accessible interface, canonicalize return values to
  ensure determinism, and ensure that reflection is consistent with the
  taming database and what is imposed upon static Joe-E code.
- There is an attack with try-finally and VirtualMachineError.
     try {
        ... X ...
     } catch (final Error reason) {
       throw JoeE.abort(reason);
     } finally {
        ... Y ...
     }
  The risk is that if an Error gets thrown when we're out of stack
  space, then the call to JoeE.abort() might fail and might cause the
  VM to throw a VirtualMachineError.  At that point the finally-clause
  (namely, Y) executes.  This is bad, because it means that Joe-E code
  (other than the abortion handler) can execute after an Error is thrown.
  For instance, Y might consume the Error and return some value or
  throw some exception.
  Attack #1: This can give access to non-determinism. e.g.,
  something like
     int f(int i) {
        try {
            f(i+1);
        } catch (final Error reason) {
            throw JoeE.abort(reason);
        } finally {
            return i;
        }
     }
  Impact: pure Joe-E code can get access to non-determinism.
  Attack #2: This can be used to attack other objects in the same
  address space and violate their object invariants.
    public class Victim {
        private int i=0, j=0; // invariant: i==j
        public void increment() {
            i++;
            call_something_trusted();
            j++;
        }
    }
    public class Attacker {
        void attack(Victim v) {
            char ignored = new char[1<<30]; // allocate lots of memory
            try {
                while (true)
                    v.increment();
            } catch (final Error reason) {
                throw JoeE.abort(reason);
            } finally {
                .. do something more with v ..
                return;
            }
        }
        // Note: when attack() returns, v's invariant is no longer valid,
        // and the Error has been consumed, and some more Joe-E code might
        // now be able to exploit a vulnerability in Victim.
    }
- Ensure that Joe-E verifier guarantees that if all constructors of
  a Java class are tamed away, then it is impossible to subclass that
  class.  For example, double-check that the Joe-E verifier does the
  right thing with default constructors (which implicitly calls the
  superclass constructor) and default calls to the superclass
  constructor (which implicitly call the superclass constructor).
- Filesystem should document internally that it is relying upon the
  assumption that the taming database has tamed away all constructors
  on File (and any subclasses).
- If we introduce an Unimplementable marker interface, we might want
  to make File be honorarily Unimplementable.
- Group had no objection to Adrian adding a delete() method to Filesystem,
  if he wants and if this does not delay release of Joe-E 1.0 library, but
  Adrian will have to test on Windows (and think carefully) to check for
  CON, PRN, PRN.TXT, and similar special filenames.
- File.list() should return ConstArray<File>, not File[].  In general
  Joe-E library should be consistent about using ConstArrays rather than
  primitive arrays, except for varargs or for where we have a good reason
  to use primitive arrays.
- Consensus: We continue to allow Object.getClass() in the taming
  database (no change).
- We need to prevent Joe-E code from implementing finalize().


We did not get around to discussing:
- org.joe_e.Filesystem
- How to think about the boundary between Joe-E and Java (e.g., powerboxes)
- "Unimplementable" marker interface, which no Joe-E code can implement
  (verifier rejects any attempt to implement it)
- Reflective access to tamed Java APIs (ensuring that reflection
  can't be used to bypass taming decisions)
- "The Deep"
- Sash powerbox for Joe-E
- Equality
- Joe-E security review


-- 
Text by me above is hereby placed in the public domain

    Cheers,
    --MarkM