This section has elaborated on some of the major areas, where the framework is currently feature incomplete. It also mentioned some places where there are unresolved issues with the model semantics. This includes problems such as missing support for the “exec” action, the missing “data actions” for access rules on possessibles and the “copy” problem.
Chapter 8
Conclusion
I believe that system models have yet to reach their full potential yet. My analysis of the current situation led me to conclude that system models needed an extensible framework to facilitate new work in this area.
Leveraging on the experiences of Joshua Bloch, I setup some guidelines for how I wanted to develop the framework. I also noticed some aspects of the current model specification language that I found inadequate.
From this I implemented a framework to work on and with system models. The framework features a parser for a revised model specification language that fixes some of the inadequacies in its predecessor. In particular, a lot of the boilerplate syntax was reduced and actor roles were added to make large scale models easier to maintain. The new language also features annotations to declare e.g. “time-cost” of actions.
Using the framework, I wrote a static reachability analysis. Emil Gurevitch wrote a simple document stealing AI. Furthermore, I wrote several basic exam-ples for solving common use cases as well as a demonstration of how to use the
“time-cost” annotation value.
While the implementation provides a foundation for working with system mod-els, it still leaves some features to be implemented, like the “execute” action
62 Conclusion
and visualisation of the models. There are also a couple of inadequacies in the language like missing data access rules and the “copy” problem.
Appendix A
Appendix
A.1 SimpleReachabilityAnalysis.java
This is full code for the “SimpleReachabilityAnalysis” class with the exception of the import-section being filtered out.
package dk . dtu . imm . s y s m o d e l . a n a l y s i s ; // [ . . . ]
/∗ ∗
∗ <p>T h i s i s a s i m p l e r e a c h a b i l i t y a n a l y s i s . Given a s e t o f
∗ c r e d e n t i a l s and a s t a r t i n g p o s i t i o n , t h i s a n a l y s i s w i l l d e d u c e
∗ what p o s i t i o n s a r e r e a c h a b l e from t h a t s t a r t i n g p o s i t i o n .
∗ Furthermore , a t e a c h r e a c h a b l e p o s i t i o n , i t w i l l d e t e r m i n e
∗ w h i c h c r e d e n t i a l s and documents a r e r e a c h a b l e t h e r e .</p>
∗
∗ XXX: C u r r e n t l y t h i s a n a l y s i s o n l y c o n s i d e r s move a c t i o n s and r e a d
∗ a c t i o n s .
∗/
@NonNullByDefault
public f i n a l c l a s s S i m p l e R e a c h a b i l i t y A n a l y s i s extends A b s t r a c t F i x P o i n t A n a l y s i s<SystemGraphNode , SystemGraphEdge ,
/∗ Marker t o k e e p i n d e n t a t i o n∗/ SystemModel , R e a c h a b i l i t y D a t a> { /∗ ∗
∗ Value f o r d e n o t i n g t h a t no c r e d e n t i a l s t o b e o b t a i n e d . T h i s
∗ i s a v a l u e ( namely , 0 ) and n o t a b i t f l a g .
∗/
64 Appendix
private s t a t i c f i n a l i n t NO NEW CREDENTIALS ON TARGET = 0 x00 ; /∗ ∗
∗ B i t f l a g t h a t d e n o t i n g t h a t t h e t a r g e t node had new
∗ c r e d e n t i a l s , b u t t h e y were n o t r e a c h a b l e .
∗/
private s t a t i c f i n a l i n t FLAG HAD UNREACHABLE CREDENTIALS = 0 x02 ; /∗ ∗
∗ B i t f l a g t h a t d e n o t i n g t h a t t h e t a r g e t c o n t a i n e d new
∗ c r e d e n t i a l s and a t l e a s t one o f them were r e a c h e d .
∗/
private s t a t i c f i n a l i n t FLAG OBTAINED NEW CREDENTIALS = 0 x01 ; /∗ ∗
∗ The minimum c r e d e n t i a l s a v a i l a b l e on t h e s t a r t i n g p o s i t i o n s
∗/
private f i n a l ImmutableSet<S y s t e m C r e d e n t i a l> i n i t i a l C r e d e n t i a l s ; /∗ ∗
∗ C r e a t e a new r e a c h a b i l i t y a n a l y s i s
∗
∗ @param i n i t i a l C r e d e n t i a l s The c r e d e n t i a l s a v a i l a b l e a t
∗ t h e s t a r t i n g p o s i t i o n .
∗ @param s t a r t P o s i t i o n The s t a r t i n g p o s i t i o n .
∗/
public S i m p l e R e a c h a b i l i t y A n a l y s i s (
I t e r a b l e<S y s t e m C r e d e n t i a l> i n i t i a l C r e d e n t i a l s , f i n a l SystemGraphNode s t a r t P o s i t i o n ) {
super( ImmutableSet . o f ( s t a r t P o s i t i o n ) , A n a l y s i s D i r e c t i o n .FORWARDS) ; t h i s. i n i t i a l C r e d e n t i a l s =
ImmutableSet . copyOf ( i n i t i a l C r e d e n t i a l s ) ; }
@Override
protected N o d e A n a l y s i s R e s u l t analyseNewNode ( SystemGraphNode node , O p t i o n a l<R e a c h a b i l i t y D a t a> i n D a t a ) {
/∗ We a r e v i s i t i n g a node f o r t h e f i r s t t i m e ∗/
R e a c h a b i l i t y D a t a d a t a ; N o d e A n a l y s i s R e s u l t r e s ; a s s e r t ! i n D a t a . i s P r e s e n t ( ) ; i f ( s t a r t N o d e s . c o n t a i n s ( node ) ) {
/∗ I t i s a s t a r t p o s i t i o n ∗/
d a t a = new R e a c h a b i l i t y D a t a ( i n i t i a l C r e d e n t i a l s ) ; /∗ I f s t a r t node h a s o t h e r s t a r t n o d e s a s n e i g h b o u r s ,
∗ u p d a t e I n p u t D a t a m i g h t l e a r n s o m e t h i n g new .
∗ ( U n l i k e l y , b u t we need i t f o r c o r r e c t n e s s )
∗/
i f ( s t a r t N o d e s . s i z e ( ) != 1 ) {
/∗ T e c h n i c a l l y , t h i s a n a l y s i s o n l y h a v e one s t a r t node ,
∗ s o t h i s c a s e i s i m p o s s i b l e . But t h i s i s an e x a m p l e
∗ and someone w i l l p r o b a b l y copy−w a s t e i t as−i s , add
∗ m u l t i p l e s t a r t n o d e s and f o r g e t a b o u t t h i s c a s e .
A.1 SimpleReachabilityAnalysis.java 65
∗
∗ To ” t h a t copy−w a s t i n g someone ” : You a r e welcome . : )
∗/
u p d a t e D a t a F r o m P r e d e c e s s o r s ( node , data , true) ; }
/∗ We a l w a y s c o n s i d e r t h e s t a r t node a s h a v i n g c h a n g e d
∗ when we v i s i t i t t h e f i r s t t i m e .
∗/
r e s = N o d e A n a l y s i s R e s u l t .CHANGED;
} e l s e {
/∗ T h i s i s a node we h a v e n o t s e e n b e f o r e and i t i s n o t
∗ a s t a r t p o s i t i o n ∗/
d a t a = new R e a c h a b i l i t y D a t a ( ) ;
/∗ We may n o t b e a b l e t o v i s i t t h i s node y e t . In t h a t c a s e ,
∗ u p d a t e D a t a F r o m P r e d e c e s s o r s w i l l r e t u r n NOT CHANGED and
∗ we w i l l j u s t r e t u r n t h a t . Our p a r e n t c l a s s w i l l t h e n
∗ ”unmark” t h e node . See t h e d o c u m e n t a t i o n o f t h e p a r e n t
∗ c l a s s f o r more i n f o r m a t i o n .
∗/
r e s = u p d a t e D a t a F r o m P r e d e c e s s o r s ( node , data , true) ; }
i f ( r e s == N o d e A n a l y s i s R e s u l t .CHANGED) {
/∗ We a r e a b l e t o v i s i t t h i s node , s o i n s e r t t h e d a t a ∗/
setNodeData ( node , d a t a ) ;
/∗ With t h e i n i t i a l c r e d e n t i a l s o b t a i n e d v i a our
∗ p r e d e c e s s o r s , s e e what we can o b t a i n from t h i s
∗ node .
∗/
u p d a t e D a t a F r o m S u c c e s s o r s ( node , d a t a ) ; }
return r e s ; }
@Override
protected N o d e A n a l y s i s R e s u l t r e a n a l y s e N o d e ( SystemGraphNode node , O p t i o n a l<R e a c h a b i l i t y D a t a> optData ) {
/∗ We h a v e p r o c e s s e d t h i s node b e f o r e ( s u c c e s s f u l l y ) . One
∗ o f our p r e d e c e s s o r s must h a v e l e a r n e d s o m e t h i n g new . ∗/
R e a c h a b i l i t y D a t a d a t a = optData . g e t ( ) ;
N o d e A n a l y s i s R e s u l t r e s = u p d a t e D a t a F r o m P r e d e c e s s o r s ( node , data , f a l s e) ;
/∗ Even i f our p r e d e c e s s o r s l e a r n e d s o m e t h i n g new , we a r e
∗ n o t a c t u a l l y g u a r a n t e e d t h a t s i t s k n o w l e d g e w i l l r e a c h
∗ t h i s node . Example :
∗
∗ p r e d e c e s s o r −−− ( i m p a s s i b l e e d g e ) −−> c u r r e n t node
∗
∗ The f i x p o i n t a n a l y s e r d o e s n o t know our c r i t e r i a f o r
∗ w h e t h e r a node i s r e a c h a b l e o r not , s o i t j u s t s u b m i t s
∗ t h e node f o r us t o p r o c e s s and l e t us d e a l w i t h i t .
∗/
i f ( r e s == N o d e A n a l y s i s R e s u l t .CHANGED) {
/∗ I f we l e a r n e d s o m e t h i n g new ( l i k e l y ) t r y t o s e e i f we
66 Appendix
∗ can o b t a i n more d a t a on t h i s node .
∗
∗ XXX: T e c h n i c a l l y , we o n l y need t o do t h i s i f we o b t a i n e d
∗ a new c r e d e n t i a l from our p r e d e c e s s o r s ( s i n c e documents
∗ do n o t ” u n l o c k ” a c c e s s t o n o d e s ) . T h i s o p t i m i s a t i o n i s
∗ l e f t a s an e x e r c i s e t o t h e r e a d e r o f t h i s comment .
∗/
u p d a t e D a t a F r o m S u c c e s s o r s ( node , d a t a ) ; }
return r e s ; }
/∗ ∗
∗ Check p r e d e c e s s o r s o f a node f o r new c r e d e n t i a l s o r documents
∗
∗ <p>When v i s i t i n g a node , i t s p r e d e c e s s o r s w i l l d e t e r m i n e w h i c h
∗ c r e d e n t i a l s and documents a r e a v a i l a b l e a t t h i s node . The s o l e
∗ e x c e p t i o n t o t h i s r u l e a r e s t a r t i n g p o s i t i o n s ( w h i c h a l w a y s
∗ h a v e t h e i n i t i a l c r e d e n t i a l s a v a i l a b l e r e g a r d l e s s o f i t s
∗ p r e d e c e s s o r s ) .
∗ </p>
∗ <p>S i n c e t h i s i s a f i x p o i n t a n a l y s i s , new k n o w l e d g e i s
∗ p r o p a g a t e d v i a n o d e s o v e r m u l t i p l e i t e r a t i o n s . T h i s method
∗ t a k e s c a r e o f r e v i e w i n g t h e p r e d e c e s s o r s f o r i n i t i a l o r new
∗ k n o w l e d g e and i n s e r t i n g i t i n t o t h e d a t a e l e m e n t f o r t h i s
∗ node .
∗ </p>
∗
∗ @param node The node b e i n g v i s i t e d .
∗ @param d a t a The a n a l y s i s d a t a f o r t h i s node . T h i s may b e
∗ u p d a t e d by t h i s c a l l .
∗ @param newNode True i f t h i s i s a new node . In t h i s c a s e , i t
∗ w i l l b e marked a s {@ l i n k N o d e A n a l y s i s R e s u l t#CHANGED}, i f i t
∗ i s r e a c h a b l e from any p r e d e c e s s o r ( e v e n i f i t p r o v i d e s no new
∗ d a t a ) .
∗ @return {@ l i n k N o d e A n a l y s i s R e s u l t#CHANGED} i f one ( o r more ) o f
∗ p r e d e c e s s o r s o f t h i s node p r o v i d e d a new c r e d e n t i a l o r document
∗ t o become a v a i l a b l e on t h i s node . R e t u r n s
∗ {@ l i n k N o d e A n a l y s i s R e s u l t#NOT CHANGED} o t h e r w i s e .
∗/
private f i n a l N o d e A n a l y s i s R e s u l t u p d a t e D a t a F r o m P r e d e c e s s o r s ( SystemGraphNode node , R e a c h a b i l i t y D a t a data ,
boolean newNode ) {
N o d e A n a l y s i s R e s u l t r e s = N o d e A n a l y s i s R e s u l t .NOT CHANGED;
P r e d i c a t e<SystemGraphNode> r e a c h a b l e P r e d = g e t S u c c e s s f u l l y V i s i t e d N o d e s P r e d i c a t e ( ) ; I t e r a b l e<? extends SystemGraphNode> p r e d e c e s s o r s =
I t e r a b l e s . f i l t e r ( node . g e t P r e d e c e s s o r N o d e s ( ) , r e a c h a b l e P r e d ) ;
f o r ( SystemGraphNode p r e d e c e s s o r : p r e d e c e s s o r s ) {
SystemGraphEdge e = p r e d e c e s s o r . g e t O u t g o i n g E d g e ( node ) ; R e a c h a b i l i t y D a t a s r c D a t a = getNodeData ( p r e d e c e s s o r ) . g e t ( ) ; i f ( ! canMoveToTarget ( e , s r c D a t a . c r e d e n t i a l s ) ) {
A.1 SimpleReachabilityAnalysis.java 67
/∗ Not p o s s i b l e t o move a c r o s s t h i s e d g e ∗/
continue; }
i f ( newNode ) {
/∗ T h i s c a s e may s e e n a b i t w e i r d , b u t i t i s a s p e c i a l
∗ c a s e f o r when t h e r e a r e no i n i t i a l c r e d e n t i a l s .
∗ In a g r a p h l i k e
∗
∗ o u t s i d e −> h a l l w a y −> . . .
∗
∗ Then i f o u t s i d e i s t h e s t a r t p o s i t i o n , t h e n i t w i l l
∗ b e u n c o n d i t i o n a l l y b e marked a s c h a n g e d ( f o r b e i n g
∗ t h e s t a r t p o s i t i o n ) .
∗
∗ But h a l l w a y w i l l n o t b e marked a s c h a n g e d i f t h e r e
∗ a r e no r e a c h a b l e c r e d e n t i a l s / documents a t ” o u t s i d e ” .
∗ The p r o b l e m i s , i f t h e r e a r e no c r e d e n t i a l
∗ r e q u i r e m e n t s f o r g o i n g from o u t s i d e t o h a l l w a y ,
∗ t h e n we s t i l l want t o s e e what we can r e a c h from
∗ h a l l w a y .
∗/
r e s = N o d e A n a l y s i s R e s u l t .CHANGED;
}
i f ( d a t a . c r e d e n t i a l s . a d d A l l ( s r c D a t a . c r e d e n t i a l s )
| | d a t a . documents . a d d A l l ( s r c D a t a . documents ) ) { r e s = N o d e A n a l y s i s R e s u l t .CHANGED;
} }
return r e s ; }
/∗ ∗
∗ Check i f new d a t a can b e o b t a i n e d from s u c c e s s o r n o d e s
∗
∗ <p>When i t h a s b e e n d e t e r m i n e d t h a t t h e c u r r e n t node h a s
∗ o b t a i n e d a new c r e d e n t i a l , t h i s method w i l l c h e c k f o r new
∗ r e a c h a b l e {@ l i n k P o s s e s s i b l e}s i n s u c c e s s o r n o d e s . I t d o e s
∗ n o t r e t u r n a {@ l i n k N o d e A n a l y s i s R e s u l t}, b e c a u s e when t h i s
∗ i s c a l l e d i t h a s a l r e a d y b e e n d e t e r m i n e d t h a t t h e c u r r e n t
∗ node h a s c h a n g e d .
∗ </p>
∗
∗ @param node The node b e i n g v i s i t e d .
∗ @param d a t a The a n a l y s i s d a t a f o r t h i s node . T h i s may b e
∗ u p d a t e d by t h i s c a l l .
∗/
private s t a t i c f i n a l void u p d a t e D a t a F r o m S u c c e s s o r s ( SystemGraphNode node , R e a c h a b i l i t y D a t a d a t a ) { I t e r a b l e<? extends SystemGraphEdge> edgesToCheck =
node . g e t O u t g o i n g E d g e s ( ) ; boolean r e c h e c k = f a l s e;
do {
/∗ Do a l i t t l e f i x p o i n t a n a l y s i s t o o b t a i n a l l c r e d e n t i a l s
∗ from s u c c e s s o r s . T h i s l i t t l e f i x p o i n t r u n s i n
68 Appendix
∗ O(|E| ∗ R) , where |E| i s t h e number o f o u t g o i n g e d g e s
∗ and R i s t h e number o f i t e r a t i o n s n e e d e d t o r e a c h a
∗ f i x p o i n t . Worst c a s e , R w i l l b e t h e number o f
∗ c r e d e n t i a l s r e a c h a b l e from t h i s node .
∗
∗ However , t h e a s s u m p t i o n i s t h a t c r e d e n t i a l s a r e n o t l y i n g
∗ around i n b i g p i l e s ( w i t h i n c r e m e n t a l a c c e s s c o n t r o l s ) .
∗ So i n p r a c t i s e , R w i l l b e f a i r l y l o w . Worst c a s e
∗ s c e n a r i o s l o o k s s o m e t h i n g l i k e t h i s :
∗
∗ s a f e 1 c o n t a i n s t h e k e y f o r s a f e 2
∗ s a f e 2 c o n t a i n s t h e k e y f o r s a f e 3
∗ . . .
∗ s a f e (N−1) c o n t a i n s t h e k e y f o r s a f e N
∗
∗ A l l s a f e s a r e r e a c h a b l e from t h e same node and we
∗ a l w a y s p r o c e s s t h e s a f e s i n t h e w o r s t p o s s i b l e
∗ o r d e r ( e . g . s t a r t i n g from s a f e N t o s a f e 1 ) .
∗
∗ k e y f o r s a f e 1 i s r e a d i l y a v a i l a b l e from t h e same node .
∗
∗ I t seemed l i k e a r i d i c u l o u s l y c a s e , s o I h a v e n o t
∗ b o t h e r e d o p t i m i s i n g t h e a l g o r i t h m f o r i t .
∗
∗ XXX: O p t i m i s i n g t h i s c o d e s o i t l e s s v u l n e r a b l e t o t h e
∗ a b o v e c a s e i s an e x e r c i s e l e f t t o t h e r e a d e r .
∗/
L i s t<SystemGraphEdge> n e x t R e c h e c k L i s t = n u l l; f o r ( SystemGraphEdge e : edgesToCheck ) {
i n t r e s u l t = f i n d N e w C r e d e n t i a l s ( e , d a t a . c r e d e n t i a l s ) ; i f ( ( r e s u l t & FLAG HAD UNREACHABLE CREDENTIALS) != 0 ) {
/∗ There were c r e d e n t i a l s l e f t on t h e t a r g e t node .
∗ Remember t h e e d g e s o we can re−p r o c e s s i t a g a i n
∗ i f we f i n d a new c r e d e n t i a l l a t e r .
∗
∗ Note we do t h i s e v e n i f
∗ FLAG OBTAINED NEW CREDENTIALS i s s e t . T h i s i s
∗ b e c a u s e f i n d N e w C r e d e n t i a l s d o e s n o t compute a
∗ f i x p o i n t ( and we a r e a l r e a d y s e t up f o r d o i n g
∗ i t anyway , s o we m i g h t a s w e l l do i t h e r e )
∗/
i f ( n e x t R e c h e c k L i s t == n u l l) {
n e x t R e c h e c k L i s t = new A r r a y L i s t< >();
}
n e x t R e c h e c k L i s t . add ( e ) ; }
i f ( ( r e s u l t & FLAG OBTAINED NEW CREDENTIALS) != 0 ) { /∗ We o b t a i n e d a new c r e d e n t i a l , s c h e d u l e a re−c h e c k
∗ i f we had any e d g e s w i t h u n r e a c h a b l e c r e d e n t i a l s .
∗
∗ NB: We d e l i b e r a t e l y do t h i s a f t e r t h e c h e c k f o r
∗ u n r e a c h a b l e c r e d e n t i a l s . ( See t h e ” u n r e a c h a b l e
∗ c r e d e n t i a l s ” c a s e a b o v e ) .
A.1 SimpleReachabilityAnalysis.java 69
∗/
r e c h e c k = n e x t R e c h e c k L i s t != n u l l; }
}
/∗ remember t o u p d a t e edgesToCheck ∗/
edgesToCheck = n e x t R e c h e c k L i s t ;
} while ( r e c h e c k && edgesToCheck != n u l l) ;
/∗ Now t h a t we o b t a i n e d a l l t h e new c r e d e n t i a l s , l o o k a t what
∗ documents we can r e a c h . We do n o t need a l l t h e h e a v y
∗ l i f t i n g o f t h e above , s i n c e documents do n o t g r a n t a c c e s s
∗ t o a n y t h i n g .
∗/
f o r ( SystemGraphEdge e : node . g e t O u t g o i n g E d g e s ( ) ) { SystemGraphNode t a r g e t = e . g e t T a r g e t N o d e ( ) ; f o r ( SystemDocument d : t a r g e t . getDocuments ( ) ) {
i f ( d a t a . documents . c o n t a i n s ( d ) ) { continue;
}
i f ( canRead ( e , d , d a t a . c r e d e n t i a l s ) ) { d a t a . documents . add ( d ) ;
} } } }
/∗ ∗
∗ Get t h e a v a i l a b l e c r e d e n t i a l s a t a g i v e n node
∗
∗ <p>T h i s method r e t u r n s t h e r e s u l t i n g </p>
∗
∗ @param node A g i v e n node
∗ @return A {@ l i n k S e t} o f t h e {@ l i n k S y s t e m C r e d e n t i a l} t h a t can
∗ b e o b t a i n e d a t t h e g i v e n node . The s e t i s u n m o d i f i a b l e . I t
∗ i s may o r may n o t b e a v i e w .
∗/
public Set<S y s t e m C r e d e n t i a l> g e t O b t a i n a b l e C r e d e n t i a l s A t N o d e (
SystemGraphNode node ) {
O p t i o n a l<R e a c h a b i l i t y D a t a> d a t a ; P r e c o n d i t i o n s . c h e c k S t a t e ( h a s S t a r t e d ( ) ,
”The a n a l y s i s h a s n o t s t a r t e d y e t ” ) ; d a t a = getNodeData ( node ) ;
i f ( ! d a t a . i s P r e s e n t ( ) ) { return ImmutableSet . o f ( ) ; }
return C o l l e c t i o n s . u n m o d i f i a b l e S e t ( d a t a . g e t ( ) . c r e d e n t i a l s ) ; }
/∗ ∗
∗ Get t h e a v a i l a b l e documents a t a g i v e n node
∗
∗ @param node A g i v e n node
∗ @return A {@ l i n k S e t} o f t h e {@ l i n k SystemDocument} t h a t can
∗ b e o b t a i n e d a t t h e g i v e n node . The s e t i s u n m o d i f i a b l e . I t
70 Appendix
∗ i s may o r may n o t b e a v i e w .
∗/
public Set<SystemDocument> getObtainableDocumentsAtNode (
SystemGraphNode node ) {
O p t i o n a l<R e a c h a b i l i t y D a t a> d a t a ; P r e c o n d i t i o n s . c h e c k S t a t e ( h a s S t a r t e d ( ) ,
”The a n a l y s i s h a s n o t s t a r t e d y e t ” ) ; d a t a = getNodeData ( node ) ;
i f ( ! d a t a . i s P r e s e n t ( ) ) { return ImmutableSet . o f ( ) ; }
return C o l l e c t i o n s . u n m o d i f i a b l e S e t ( d a t a . g e t ( ) . documents ) ; }
/∗ ∗
∗ T e s t i f a p o s s e s s i b l e can b e r e a d from an e d g e .
∗
∗ <p>H e l p e r method t o k e e p l e n g t h o f l i n e s down and c o n d i t i o n s
∗ s i m p l e .</p>
∗
∗ @param e An e d g e
∗ @param p A p o s s e s s i b l e on t h e t a r g e t node o f t h e e d g e
∗ @param c r e d s A s e t o f c r e d e n t i a l s
∗ @return t r u e i f p can b e r e a d o v e r e w i t h t h e g i v e n c r e d e n t i a l s
∗/
private s t a t i c f i n a l boolean canRead ( SystemGraphEdge e , P o s s e s s i b l e p , Set<S y s t e m C r e d e n t i a l> c r e d s ) { boolean copy = e . h a s S u f f i c i e n t C r e d e n t i a l s (
A c t o r A c t i o n T y p e . INPUT COPY, p , c r e d s ) ; i f ( copy ) {
return true; }
return e . h a s S u f f i c i e n t C r e d e n t i a l s (
A c t o r A c t i o n T y p e . INPUT ORIGINAL , p , c r e d s ) ; }
/∗ ∗
∗ T e s t i f i t i s p o s s i b l e t o move o v e r a g i v e n e d g e
∗
∗ <p>H e l p e r method t o k e e p l e n g t h o f l i n e s down and c o n d i t i o n s
∗ s i m p l e .</p>
∗
∗ @param e An e d g e
∗ @param c r e d s A s e t o f c r e d e n t i a l s
∗ @return t r u e i f i t i s p o s s i b l e t o move o v e r e w i t h t h e g i v e n
∗ c r e d e n t i a l s
∗/
private s t a t i c f i n a l boolean canMoveToTarget ( SystemGraphEdge e , Set<S y s t e m C r e d e n t i a l> c r e d s ) {
return e . i s A c t i o n T y p e P o s s i b l e ( A c t o r A c t i o n T y p e .MOVE)
&& e . h a s S u f f i c i e n t C r e d e n t i a l s (
A c t o r A c t i o n T y p e .MOVE, c r e d s ) ; }
A.1 SimpleReachabilityAnalysis.java 71
/∗ ∗
∗ Check a t a r g e t node f o r new c r e d e n t i a l s
∗
∗ @param e The b e t w e e n t h e c u r r e n t node ( s o u r c e ) and t h e t a r g e t
∗ node p o s s i b l y c o n t a i n i n g new c r e d e n t i a l s .
∗ @param c r e d s A m u t a b l e s e t c o n t a i n i n g t h e c u r r e n t a v a i l a b l e
∗ c r e d e n t i a l s . I t w i l l b e u p d a t e d i f new c r e d e n t i a l s become
∗ a v a i l a b l e .
∗ @return E i t h e r {@ l i n k #NO NEW CREDENTIALS ON TARGET} o r a b i t
∗ mask o f c o n t a i n i n g one o r more o f
∗ {@ l i n k #FLAG OBTAINED NEW CREDENTIALS} and
∗ {@ l i n k #FLAG HAD UNREACHABLE CREDENTIALS}.
∗ <p><em>Note</em>: I f b o t h
∗ {@ l i n k #FLAG HAD UNREACHABLE CREDENTIALS} and
∗ {@ l i n k #FLAG OBTAINED NEW CREDENTIALS} a r e s e t i n t h e r e t u r n
∗ v a l u e , i t may b e p o s s i b l e t h a t a r e p e a t e d c a l l t o t h i s method
∗ w i l l o b t a i n a n o t h e r c r e d e n t i a l .</p>
∗/
private s t a t i c f i n a l i n t f i n d N e w C r e d e n t i a l s ( SystemGraphEdge e , Set<S y s t e m C r e d e n t i a l> c r e d s ) {
SystemGraphNode t a r g e t = e . g e t T a r g e t N o d e ( ) ; i n t r e s u l t = NO NEW CREDENTIALS ON TARGET ;
f o r ( S y s t e m C r e d e n t i a l c : t a r g e t . g e t C r e d e n t i a l s ( ) ) { i f ( c r e d s . c o n t a i n s ( c ) ) {
continue; }
i f ( canRead ( e , c , c r e d s ) ) {
/∗ T h i s c r e d e n t i a l c o u l d g i v e us a c c e s s t o a n o t h e r
∗ c r e d e n t i a l a c c e s s i b l e from t h i s node ( i . e . we o u g h t
∗ re−c h e c k a l l u n r e a c h a b l e c r e d e n t i a l s on t h i s node ) .
∗ Though c r e d e n t i a l s a r e u n l i k e l y t o l i e around i n
∗ b i g p i l e s , s o we r e l y on our c a l l e r ( s ) t o c a l l us
∗ a g a i n u n t i l t h e y a r e happy .
∗
∗ They p r e t t y much h a v e t o any way , s i n c e someone
∗ c o u l d w r i t e a model where l i k e t h i s :
∗
∗ s a f e 1 c o n t a i n s a l l odd numbered k e y s b e t w e e n
∗ 1 and N
∗ s a f e 2 c o n t a i n s a l l e v e n numbered k e y s b e t w e e n
∗ 1 and N
∗
∗ To r e a c h keyX , you need k e y (X−1).
∗ Agent s t a r t s w i t h k e y 0 .
∗
∗ In t h i s c a s e , you would ( s t i l l ) need N c a l l s t o
∗ t h i s method t o o b t a i n them a l l . I b e l i e v e d t h i s
∗ c a s e was p r e t t y ” u n l i k e l y ” i n any ” r e a l ” use , s
∗ I h a v e n o t o p t i m i s e d f o r i t . See a l s o t h e comment
∗ w o r s t c a s e r u n t i m e i n u p d a t e D a t a F r o m S u c c e s s o r s .
∗/
c r e d s . add ( c ) ;
r e s u l t |= FLAG OBTAINED NEW CREDENTIALS ;
72 Appendix
} e l s e {
r e s u l t |= FLAG HAD UNREACHABLE CREDENTIALS ; }
}
return r e s u l t ; }
}
/∗ C l a s s h o l d i n g t h e d a t a o b t a i n e d f o r a g i v e n node . I t s v i s i b i l i t y
∗ o u t s i d e t h i s c l a s s f i l e i s n o t n e e d e d ( i n p a r t i c u l a r , our
∗ consumers need n o t know o f i t .
∗
∗ S i n c e i t i s an i m p l e m e n t a t i o n d e t a i l , t h e c l a s s a b o v e g e t s t o
∗ a c c e s s t h e members d i r e c t l y i n s t e a d o f u s i n g ” a c c e s s o r s ” .
∗/
f i n a l c l a s s R e a c h a b i l i t y D a t a {
/∗ r e a c h a b l e / o b t a i n a b l e documents a t t h i s node ∗/
f i n a l Set<SystemDocument> documents = new HashSet< >();
/∗ r e a c h a b l e / o b t a i n a b l e c r e d e n t i a l s a t t h i s node ∗/
f i n a l Set<S y s t e m C r e d e n t i a l> c r e d e n t i a l s ; R e a c h a b i l i t y D a t a ( ) {
c r e d e n t i a l s = new HashSet< >();
}
R e a c h a b i l i t y D a t a ( Set<S y s t e m C r e d e n t i a l> i n i t i a l C r e d e n t i a l s ) { c r e d e n t i a l s = new HashSet<>( i n i t i a l C r e d e n t i a l s ) ;
} }