added lectures 2 and 3

Myers/Battleship.jif

@@ -0,0 +1,107 @@
+import java.io.PrintStream;
+
+/**
+ * The class BattleShip is responsible for coordinating gameplay
+ * between two Players, P1 and P2.
+ */
+class BattleShip[principal P1, principal P2] authority (P1, P2) {
+    /**
+     * The number of covered coordinates that each player is to 
+     * have on their board. Players can have any number of ships,
+     * so long as the ships cover this number of squares.
+     */
+    public static final int{*<-*} NUM_COVERED_COORDS = 10;
+
+    public void play{P1<-* meet P2<-*}(PrintStream[{}]{P1<-* meet P2<-*} output) 
+      throws (SecurityException, IllegalArgumentException{P1<-* meet P2<-*})
+      where authority (P1, P2) {
+
+        if (output == null) throw new IllegalArgumentException("Null output");
+
+
+        output.println("Playing battleships, with each player having " 
+                       + NUM_COVERED_COORDS + " covered coordinates");
+
+        // instantiate the two players
+        Player[P1,P2] player1 = new Player[P1,P2]();
+        Player[P2,P1] player2 = new Player[P2,P1]();
+
+
+
+        // Initialize the two players.
+        output.print("  Initializing....");
+
+        // Player 1 first creates a board
+        Board[{P1->*;P1<-*}] proposed1 = player1.init(NUM_COVERED_COORDS);
+
+        // Player 2 endorses it (since Player 2 doesn't care where the 
+        // pieces are located).
+        Board[{P1->*;P1<-* meet P2<-*}] accepted1 = player2.endorseBoard(proposed1);
+
+        // Player 1 stores the endorsed board.
+        player1.storeBoard(accepted1);
+
+        // Similarly for Player 2: create a board, Player 1 endorses, and board 
+        // is stored.
+        Board[{P2->*;P2<-*}] proposed2 = player2.init(NUM_COVERED_COORDS);
+        Board[{P2->*;P2<-* meet P1<-*}] accepted2 = player1.endorseBoard(proposed2);
+        player2.storeBoard(accepted2);
+
+        output.println(" Done.");
+
+        // These fields record how many hits each player has scored.
+        // The game continues until one of the players has
+        // scored NUM_COVERED_COORDS hits.
+        int player1Hits = 0;
+        int player2Hits = 0;
+
+        output.println("  Playing rounds...");
+
+        // loop until a player hits all the covered co-ordinates.
+        while (player1Hits < NUM_COVERED_COORDS && player2Hits < NUM_COVERED_COORDS) {
+
+            // get player 1's query
+            Coordinate[{P1<-*}] play1Query = player1.getNextQuery();
+
+            // Player 1's query is endorsed by Player 2.
+            Coordinate[{P1<-* meet P2<-*}] play1QueryEnd = player2.endorseQuery(play1Query);
+
+            output.print("\t"+PrincipalUtil.toString(P1)+": " + 
+			 (play1QueryEnd==null?"null":play1QueryEnd.toString()) + 
+                         "?  " );
+
+            // Player 2 processes Player 1's query
+            boolean result = player2.processQuery(play1QueryEnd);
+            player1Hits += result ? 1 : 0;
+            output.print((result?"Y":"N"));
+
+
+            if (player1Hits < NUM_COVERED_COORDS) {
+                // player 1 hasn't won, so let player 2 ask a query...
+                Coordinate[{P2<-*}] play2Query = player2.getNextQuery();
+
+                //player 1 endorse's the query
+                Coordinate[{P1<-* meet P2<-*}] play2QueryEnd = player1.endorseQuery(play2Query);
+
+                output.print("   "+PrincipalUtil.toString(P2)+": " + 
+			     (play2QueryEnd==null?"null":play2QueryEnd.toString()) 
+                             + "?  ");
+
+                // get player 1 to process player 2's query
+                boolean result2 = player1.processQuery(play2QueryEnd);
+
+                player2Hits += result2 ? 1 : 0;       
+                output.print((result2?"Y":"N"));
+
+                // print a running total of the scores...
+                output.println("   Score: " + player1Hits + " vs. " + player2Hits);
+            }
+        }
+
+        // Let's see who won...
+        output.println("\n");
+        output.println((player1Hits >= NUM_COVERED_COORDS ? PrincipalUtil.toString(P1) 
+                                                          : PrincipalUtil.toString(P2)) 
+                       + " won!");
+    }
+}

Myers/Hello.jif

@@ -0,0 +1,16 @@
+import java.io.PrintStream;
+import jif.runtime.Runtime;
+
+// compile with -fail-on-exception
+public class Hello
+{
+    public Hello() {}
+    public static void main{}(principal{pp<-} pp,
+                              String[]{} args)
+        throws (SecurityException, NullPointerException)
+    {
+        Runtime runtime = Runtime[pp].getRuntime();
+        PrintStream out = runtime.out();
+        out.println("Hello, world!");
+    }
+}

Myers/bib.bib

@@ -0,0 +1,49 @@
+@article{chong2007secure,
+  title={Secure web applications via automatic partitioning},
+  author={Chong, Stephen and Liu, Jed and Myers, Andrew C and Qi, Xin and Vikram, Krishnaprasad and Zheng, Lantian and Zheng, Xin},
+  journal={ACM SIGOPS Operating Systems Review},
+  volume={41},
+  number={6},
+  pages={31--44},
+  year={2007},
+  publisher={ACM},
+  url={http://www.cs.cornell.edu/andru/papers/swift-sosp07.pdf}
+}
+
+@article{zdancewic2001untrusted,
+  title={Untrusted hosts and confidentiality: Secure program partitioning},
+  author={Zdancewic, Steve and Zheng, Lantian and Nystrom, Nathaniel and Myers, Andrew C},
+  journal={ACM SIGOPS Operating Systems Review},
+  volume={35},
+  number={5},
+  pages={1--14},
+  year={2001},
+  publisher={ACM},
+  url={http://www.cs.cornell.edu/andru/papers/sosp01/zznm01.pdf}
+}
+
+@article{volpano1996sound,
+  title={A sound type system for secure flow analysis},
+  author={Volpano, Dennis and Irvine, Cynthia and Smith, Geoffrey},
+  journal={Journal of computer security},
+  volume={4},
+  number={2-3},
+  pages={167--187},
+  year={1996},
+  publisher={IOS Press},
+  url={http://users.cis.fiu.edu/~smithg/papers/jcs96.pdf}
+}
+
+@article{pottier2003information,
+  title={Information flow inference for {ML}},
+  author={Pottier, Fran{\c{c}}ois and Simonet, Vincent},
+  journal={ACM Transactions on Programming Languages and Systems (TOPLAS)},
+  volume={25},
+  number={1},
+  pages={117--158},
+  year={2003},
+  publisher={ACM},
+  url={http://www.normalesup.org/~simonet/publis/fpottier-simonet-toplas.pdf}
+}
+
+

Myers/bib2.bib

@@ -0,0 +1,61 @@
+@article{zdancewic2001robust,
+  title={Robust Declassification.},
+  author={Zdancewic, Steve and Myers, Andrew C},
+  booktitle={csfw},
+  volume={1},
+  pages={15--23},
+  year={2001},
+  organization={Citeseer}
+}
+
+
+
+@inproceedings{zdancewic2003observational,
+  title={Observational determinism for concurrent program security},
+  author={Zdancewic, Steve and Myers, Andrew C},
+  booktitle={16th IEEE Computer Security Foundations Workshop, 2003. Proceedings.},
+  pages={29--43},
+  year={2003},
+  organization={IEEE}
+}
+
+@inproceedings{zdancewic2001robust,
+  title={Robust Declassification.},
+  author={Zdancewic, Steve and Myers, Andrew C},
+  booktitle={csfw},
+  volume={1},
+  pages={15--23},
+  year={2001},
+  organization={Citeseer}
+}
+
+@inproceedings{roscoe1995csp,
+  title={CSP and determinism in security modelling},
+  author={Roscoe, A William},
+  booktitle={Proceedings 1995 IEEE Symposium on Security and Privacy},
+  pages={114--127},
+  year={1995},
+  organization={IEEE}
+}
+
+@inproceedings{charles2005x10,
+  title={X10: an object-oriented approach to non-uniform cluster computing},
+  author={Charles, Philippe and Grothoff, Christian and Saraswat, Vijay and Donawa, Christopher and Kielstra, Allan and Ebcioglu, Kemal and Von Praun, Christoph and Sarkar, Vivek},
+  booktitle={Acm Sigplan Notices},
+  volume={40},
+  number={10},
+  pages={519--538},
+  year={2005},
+  organization={ACM}
+}
+
+@article{milanova2005parameterized,
+  title={Parameterized object sensitivity for points-to analysis for Java},
+  author={Milanova, Ana and Rountev, Atanas and Ryder, Barbara G},
+  journal={ACM Transactions on Software Engineering and Methodology (TOSEM)},
+  volume={14},
+  number={1},
+  pages={1--41},
+  year={2005},
+  publisher={ACM}
+}