Read Me

======================= JavaHBAC =======================
Edited by Karl Krukow (karl.krukow@gmail.com),
Sun Feb 11 13:39:45 CET 2007
========================================================

----------------- Preliminaries --------------
The JavaHBAC system is at a prototype stage of development. This means
that there is a considerable amount of work needed in order to use the
system. However, the basic components are available so that advanced
developers can build on these.

Users should read the paper,

[1] "A Logical Framework for Reputation Systems and History-based Access Control",
	to be published in Journal of Computer Security (http://www.mitre.org/public/jcs/)
	in 2007
	Preprint is available online at:
    http://www.brics.dk/~krukow

It has a brief section describing the system and the necessary
background. No further documentation is currently available.       



Dependencies.

JavaHBAC is developed using features of Java 5.0, hence the classes work
only with 

- Java JDK 5.0 (Tiger) or later.

Further, the following Java packages must be installed to use the
system. 

- DSD2.0 available from 
  http://www.brics.dk/DSD/dsd2/

- dk.brics.automaton package, available from
  http://www.brics.dk/automaton/ 

- JavaBDD - Binary Decision Diagrams for Java, available from
  http://javabdd.sourceforge.net/

- Our use of the JavaBDD package requires that the libbuddy.so file is
  in the current directory (when using Linux). This file is also
  included in the lib directory.


Please read the documentation of these packages for installation and
for usage instructions.

----------------- Use of JavaHBAC --------------

The JavaHBAC package contains a policy language for specifying
access-control policies, as well as algorithms for enforcing such
policies. The package is intended to be used when writing customised
Java Security Managers. For example, we have implemented a simple
security manager which gets a policy as input and then monitors the
run of a target java program, enforcing the input-policy.  
In the section denoted "An Example" we show how this security manager
can be run.  

More specifically, JavaHBAC consists of the following components:

  (i) An XML language for writing History-based Access Control
      policies for Java applications. The language is meant to be used
      for experimentation with the JavaHBAC system, therefore it
      handles only a few select security events (regarding file and
      network access). 

      It is hoped that other interested developers will extend the
      language to a useful and complete language for specifying
      History-Based Access Control Policies.

      The language is defined using the formal language DSD2.0. The
      schema is located in the file DSD2.0/quantifiedjavapolicies.dsd

      An example policy is found in:
      examples/policies/Quantified_File-Example.xml


 (ii) Java classes for representing the abstract syntax of policies in
      language. 

      See the directory:
      dk/brics/javahbac/policylanguage/syntax
      
      In fact there are two languages: a basic and a parameterised or
      quantified language. 

(iii) A simple (almost naive) SAX parser which parses an XML policy in
      the language and constructs an internal representation of the
      policy using the Abstract syntax.

      See the directory:
      dk/brics/javahbac/policylanguage/parsing

The above three components hence deals with policy specification and
policy representation in Java.

The main classes in the JavaHBAC implements algorithms (described in
reference [1]) for dynamic model checking .



 (iv) Two algorithms for Dynamic Model Checking, i.e., for
      enforcing policies, are implemented. 
      (See [1] or dk/brics/javahbac/dmc/DynamicModelChecker.java)

      For the XML language, one may use:
      dk/brics/javahbac/dmc/ArrayBasedDMC.java
      
      Which implements the array-based algorithm using constraints
      (see [1]).

      The BDD-Based constraint-implementation is located in:
      dk/brics/javahbac/util/BDDConstraint.java

      The other algorithm is for non-quantified policies and uses
      finite automata. This implementation is located in:
      dk/brics/javahbac/dmc/ArrayBasedDMC.java/AutomataBasedDMC.java
 




----------------- An Example --------------

We have implemented a very simple example security manager (QSecMan)
and a test-example (TestQSecMan).

The example can be run by doing the following from the HBAC 
root-directory. 


   * Make sure your classpath contains the JavaBDD jar as well as the
     other dependency jars. (For convenience use the lib dir, and set
     your CLASSPATH variable to point to all .jar files in that
     directory).

   * change current working directory to the "tryatonce" subdirectory.

   * run the TestQSecMan class with the Quantified_File-Example.xml
     policy and parameter "evil".

        [krukow@thyra02:...javahbac/tryatonce]$ java -cp $CLASSPATH:javahbac-0.4-1.jar dk.brics.javahbac.testing.securitymanagers.TestQSecMan Quantified_File-Example.xml evil
      

The following output should be generated:

Setting Security Manager
[...]
Starting Program
begin
check: (java.util.PropertyPermission user.dir read)
check: (java.io.FilePermission secret.txt read)
after filereader
thesecretpassWord
after out
check: (java.util.PropertyPermission java.net.preferIPv6Addresses read)
check: (java.lang.RuntimePermission loadLibrary.net)
[...]
check: (java.net.SocketPermission www.microsoft.com resolve)
Exception in thread "main" java.lang.SecurityException: Execution History Exception: Neg(QSince(QTrue, Neg(QForall x.(Neg(Conj(Event((java.io.FilePermission x read)(x)), Neg(QSince(QTrue, Event((java.io.FilePermission x write)(x))))))))))        at QSecMan.checkPermission(QSecMan.java:37)
[...]


   * Now try and run the TestQSecMan class parameter "good" (or any other).

      -  [krukow@thyra02:...javahbac/tryatonce]$ java -cp $CLASSPATH:javahbac-0.4-1.jar dk.brics.javahbac.testing.securitymanagers.TestQSecMan Quantified_File-Example.xml good

The following output should be generated:

Setting Security Manager
check: (java.security.SecurityPermission getProperty.networkaddress.cache.ttl)
check: (java.util.PropertyPermission sun.net.inetaddr.ttl read)
check: (java.security.SecurityPermission getProperty.networkaddress.cache.negative.ttl)
Starting Program
check: (java.io.FilePermission /home/java/Linux-jdk1.5.0_04/jre/lib/i386/libnet.so read)
check: (java.util.PropertyPermission user.dir read)
check: (java.io.FilePermission tmp.txt write)
check: (java.util.PropertyPermission line.separator read)
check: (java.util.PropertyPermission java.net.preferIPv6Addresses read)
check: (java.lang.RuntimePermission loadLibrary.net)
check: (java.io.FilePermission /home/java/Linux-jdk1.5.0_04/jre/lib/i386/libnet.so read)
check: (java.util.PropertyPermission java.net.preferIPv4Stack read)
check: (java.util.PropertyPermission impl.prefix read)
check: (java.lang.reflect.ReflectPermission suppressAccessChecks)
check: (java.util.PropertyPermission sun.net.spi.nameservice.provider.1 read)
check: (java.net.SocketPermission www.microsoft.com resolve)
check: (java.lang.RuntimePermission loadLibrary.net)
check: (java.io.FilePermission /home/java/Linux-jdk1.5.0_04/jre/lib/i386/libnet.so read)
check: (java.net.SocketPermission 207.46.199.30:80 connect,resolve)
check: (java.net.SocketPermission 207.46.199.30:80 connect,resolve)
check: (java.util.PropertyPermission java.home read)
check: (java.io.FilePermission /home/java/Linux-jdk1.5.0_04/jre/lib/net.properties read)
check: (java.util.PropertyPermission java.net.useSystemProxies read)
check: (java.lang.reflect.ReflectPermission suppressAccessChecks)
check: (java.net.NetPermission getProxySelector)
check: (java.util.PropertyPermission socksProxyHost read)
OK!


Explanation:

 The program QSecMan installs a security manager which enforces the
 input policy (Quantified_File-Example.xml). The program the proceeds depending
 on the second parameter ("evil" or "good").

 The policy Quantified_File-Example.xml specifies that the program cannot
 connect to a site if it has read a file that is different from

 /home/java/Linux-jdk1.5.0_04/jre/lib/i386/libnet.so

 (this file is necessary for internet access, you might need to chose
 a different file if you are not using Linux or the libnet.so is
 located elsewhere).


 If the second parameter is "evil" then it runs a program that tries
 to open the local file "secret.txt" and the proceed to open a
 connection to www.microsoft.com 

 otherwise it runs a "non-malicious program" which simply opens a
 connection to www.microsoft.com

Note that an exception is thrown if the "evil" program is run, while
no exception is thrown if the "good" program is run.


Experimentation with JavaHBAC is probably best done by starting to
modify and play with these example programs. 






------------- Bugs/Features -------------


 - There is a "feature" of Java which may cause a class circularity
   error when a security manager causes a class to be loaded.
   consider the code of TestQSecMan.java


import java.util.*;
import java.security.Permission;

public class TestQSecMan {
    public static void main(String[] args) throws Exception {
	InductiveQSemantics<Perm> s = new InductiveQSemantics<Perm>(null,null,null,null,null,null);// hack
	PEvent<Object> p = new PEvent<Object>(new Object(),new Par(null));// hack

	QPolicyParser pp = new QPolicyParser();
	pp.parse(args[0]);
 
	QSecMan sec = setupSecurityManager(pp);
	System.out.println("Setting Security Manager");
	System.setSecurityManager(sec);
	System.out.println("Starting Program");
	Evil.main(null);
    }
    private static QSecMan setupSecurityManager(QPolicyParser pp) {
	HashMap<Action,QFormula<Perm>> act_for =  pp.getActFor();
 	HashSet<PEvent<Perm>> events = pp.getEvents();
 	HashSet<Action> actions = pp.getActions();
 	SimpleJavaPES<Perm> es = new SimpleJavaPES<Perm>(events);
	return new QSecMan(act_for,events,actions);
    
    }
}

  Note in particular that the following two lines are included to
  circumvent this error (by causing the classes to be loaded
  before the security manager is run).
  
  InductiveQSemantics<Perm> s = new InductiveQSemantics<Perm>(null,null,null,null,null,null);// hack
  PEvent<Object> p = new PEvent<Object>(new Object(),new Par(null));//  hack

  The "Bug/Feature" has been reported to Sun.





Good Luck. 

Please report errors and post questions to karl.krukow@gmail.com

Regards,
- Karl Krukow