I. Alloy Analysis Tool A. What is the Alloy Analysis Tool ------------------------------------------ WHAT IS ALLOY? Tool for: - domain modeling - abstractly investigating designs - systematic testing, within a size limit ------------------------------------------ B. Ideas behind Alloy ------------------------------------------ APPROACH USED BY ALLOY - Everything is a relation (or an atom) - General logic - Check specified properties using bounded search for counterexamples - Technique used is SAT solving ------------------------------------------ Isn't SAT exponential? ------------------------------------------ SMALL SCOPE HYPOTHESIS "Most flaws in models can be illustrated by small instances" - Daniel Jackson ------------------------------------------ C. Semantics of Alloy 1. Atoms ------------------------------------------ ATOMS Atoms are: - just names, i.e. modeling abstractions ------------------------------------------ 2. All values are relations ------------------------------------------ ALL VALUES ARE RELATIONS Universe is n-ary relations Relations model: - all data types including: - sets - scalars - tuples -- structures in space and time N-ary Relations are: sets of n-tuples (of atoms) No distction between: - a scalar - a singleton set - a unary tuple - a relation Columns identified by position (not names) Example: Binary relation from names to addresses module relationBasics sig Name, Addr {} one sig Book { addr: Name -> lone Addr } pred show(){} run show ------------------------------------------ a. views of relations ------------------------------------------ VIEWS OF RELATIONS Can think in these styles: - predicate calculus: all n:Name, a1, a2: Addr | n->a1 in Book.addr and n->a2 in Book.addr implies (a1 = a2) - navigational: all n: Name | lone Book.addr[n] - relational: all n: Name | lone n.Book.addr ------------------------------------------ b. relational join ------------------------------------------ RELATIONS AND DOT JOIN (.) Key operator is dot (.) where s.t (or t[s]) is the join of the last column of s with the first column of t If (s1->s2->...->sN-1->sN) in s and (t1->t2->...->tM) in t then (s1->s2->...sN-1->t2->...tM) in s.t iff sN = t1 used for: - relational join - field navigation - function composition - function application ------------------------------------------ How is the join of binary relations defined? ------------------------------------------ SPECIAL CASES OF JOIN For binary relations, as in set theory: (a,c) in (R . S) <==> exists b :: (a,b) in R and (b,c) in S. When F is functional, A is unary: A.F = F[A] = {(b)| (a,b) in F, a in A } ------------------------------------------ ------------------------------------------ JOIN IN ALLOY module joining sig S, T{} assert basicJoinProperty { all s1:univ, s2: univ, t1: univ, t2: univ | let sTuple = s1 -> s2 { let tTuple = t1 -> t2 { (s1-> t2) = sTuple.tTuple iff (s2 = t1) // note: // sTuple.tTuple = tTuple[sTuple] } } } check basicJoinProperty ------------------------------------------ What happened to s2 and t1? ------------------------------------------ WHY USE RELATIONS? Easy to understand: - Relations directly model: graphs, functions - Relations are first order, so tractable to analyze - Uniform syntax ------------------------------------------ 3. General logic ------------------------------------------ NO SPECIALIZED LOGIC No special cases in logic for: - state machines, - traces, - synchronization, - concurrency, - etc. ------------------------------------------ 4. Analysis via bounded search for counterexamples ------------------------------------------ ANALYSIS VIA BOUNDED SEARCH Experience shows that: - most assertions are wrong - most counterexamples are small So analyzer tests: - completely within a small bound ------------------------------------------ What do we mean by testing completeley within a small bound? D. extended example ------------------------------------------ MODELING THE E-COMMERCE PAPER'S ATTACKS Want to formally model attacks in: Rui Wang, Shuo Chen, XiaoFeng Wang, and Shaz Qadeer. How to Shop for Free Online -- Security Analysis of Cashier-as-a-Service Based Web Stores. In IEEE Symposium on Security and Privacy, 2011, pp. 465-480. doi: 10.1109/SP.2011.26 ------------------------------------------ 1. domain modeling ------------------------------------------ DOMAIN MODELING module logicalProblems open util/ordering[Time] as TO open util/ordering[State] as SO sig Time {} sig Value {} sig OnlineEntity {} sig TStore, CaaS, Attacker extends OnlineEntity {} sig Message { sender, receiver: OnlineEntity, val: Value }{ sender != receiver } sig Signed extends Message { signedBy: OnlineEntity } sig State { sent: Message -> Time } // initial state of the system pred init [t: Time] { State.sent.t = none } pred step[t: Time, pre: State, m: Message, post: State, t2: Time] { lt[t,t2] => (pre.sent.t + m) = post.sent.t2 } fact traces { init [first] all t: Time-last | let t2 = t.next | all m: Message | all s,s2: State | s2 in s.next and m in s.sent.t => step [t, s, m, s2, t2] } pred show() {} run show ------------------------------------------ 2. modeling an attack ------------------------------------------ MODELING AN ATTACK Want traces to show the attack, then look to see if there is a trace where security property violated Steps: - Model domains involved: - Online Entities modeled as Sigs - Attacker, - TStore, - CaaS - Messages fields: - sender, receiver, value - signed messages (a subtype) - identity of the signer - extract properties with functions e.g., originator of value - States - sequence of messages sent ------------------------------------------ What do signatures correspond to? ------------------------------------------ ATTACK AS FACT ABOUT STATES module eCommerceFig4Better open logicalProblems as LP fact { all t0: LP/Time | init[t0] and let t1a = t0.next | let t1b = t1a.next | let t2a = t1b.next | let t2b = t2a.next | let t3a = t2b.next | let t3aa = t3a.next | let t3ab = t3aa.next | let t3b = t3ab.next | all s0: LP/State | let s1a = s0.next | let s1b = s1a.next | let s2a = s1b.next | let s2b = s2a.next | let s3a = s2b.next | let s3aa = s3a.next | let s3ab = s3aa.next | let s3b = s3ab.next | all m1a,m1b,m2a,m2b,m3a,m3aa,m3ab,m3b: Message | m1a.sender = LP/Attacker and m1a.receiver = LP/TStore and m1b.sender = LP/TStore and m1b.receiver = LP/Attacker and m2a.sender = LP/Attacker and m2a.receiver = LP/CaaS and m3a.sender = LP/Attacker and m3a.receiver = LP/TStore and m3aa.sender = LP/TStore and m3aa.receiver = LP/CaaS and m3ab.sender = LP/CaaS and m3ab.receiver = LP/TStore and m3b.sender = LP/TStore and m3b.receiver = LP/Attacker and step[t0,s0,m1a,s1a,t1a] and step[t1a, s1a, m1b, s1b, t1b] and step[t1b,s1b,m2a,s2a,t2a] and step[t2a, s2a, m2b, s2b, t2b] and step[t2b,s2b,m3a,s3a,t3a] and step[t3a, s3a, m3aa, s3aa, t3aa] and step[t3aa,s3aa,m3ab,s3ab,t3ab] and step[t3ab, s3ab, m3b, s3b, t3b] => s1a.sent.t1a = m1a and s1b.sent.t1b = m1a+m1b and s2a.sent.t2a = m1a+m1b+m2a and s2b.sent.t2b = m1a+m1b+m2a+m2b and s2b.sent.t2b = m1a+m1b+m2a+m2b+m3a and s3a.sent.t3a = m1a+m1b+m2a+m2b+m3a+m3aa and s3aa.sent.t3aa = m1a+m1b+m2a+m2b+m3a+m3aa+m3ab and s3ab.sent.t3ab = m1a+m1b+m2a+m2b+m3a+m3aa+m3ab+m3b } pred show{} run show for 10 Time, 8 LP/Value, 3 LP/OnlineEntity, 8 LP/Message, 6 LP/State ------------------------------------------ 3. formulating security properties What security policies should be enforced? II. Using Alloy to Develop a Model of E-Commerce A. type basics for Alloy 1. Recap of relational join ------------------------------------------ RELATIONS AND DOT JOIN (.) Dot operator (.) does a relational join i.e., s.t is the join of the last column of s with the first column of t If (s1->s2->...->sN-1->sN) in s and (t1->t2->...->tM) in t then (s1->s2->...sN-1->t2->...tM) in s.t iff sN = t1 Also, note that s.t = t[s] ------------------------------------------ ------------------------------------------ UNDERSTANDING DECLARATIONS AND JOINS Consider module TypingBasicsSigs sig A,B,C,D,E {} sig Rel { r: A -> B -> C, s: C -> D -> E } Rules of thumb: Let r = Rel.r | if a: A, b: B, c: C, then: r : A -> B -> C r.c : A -> B r.c.b : A So dot (.) Similarly: r : A -> B -> C r[a] : B -> C r[a][b] : C So [] ------------------------------------------ 2. domain and range ------------------------------------------ DOMAIN AND RANGE OF A RELATION Note: univ means Signatures also denote Can apply a relation to a set suppose f: A -> B, then f[A] = { b | a in A, (a->b) in f } What is f[univ]? What is f.B? Suppose r: A -> B -> C, What expression would give the set { b | a in A, c in C, (a -> b -> c) in r } ? What expression would give r's domain? ------------------------------------------ B. modeling tips ------------------------------------------ FAILED APPROACH (TUESDAY) 1. specify signatures 2. specify predicates for scenarios Problems: - not clear how to find/specify security policies or violations - formulas unwieldy/complex so too long to execute - some information redundantly specified ------------------------------------------ 1. better approach a. use events ------------------------------------------ BETTER APPROACH (1): USE EVENTS Events help avoid redundancies: - time vs. messages - time vs. states So events contain: - time - message information Abstractly, start with time: module Event[Time] // events are transitions that // start at time pre and end at time post abstract sig Event { pre, post: Time } ------------------------------------------ Does each event take a finite amount of time? b. constrain time and events ------------------------------------------ CONSTRAIN TIME AND EVENTS module Shimanto[Time] // Adapted from CODE 1 in the paper // H. Shimamoto, N. Yanai, S. Okamura, // J. P. Cruz, S. Ou and T. Okubo, // "Towards Further Formal Foundation // of Web Security: // Expression of Temporal Logic in Alloy // and Its Application // to a Security Model With Cache," // in IEEE Access, vol. 7, // pp. 74941-74960, 2019, // doi: 10.1109/ACCESS.2019.2920675. open util/ordering[Time] open Event[Time] fact Traces { // 1 all t:Time-last | one e:Event | e.pre=t and e.post=t.next // 2 all e:Event | e.post=e.pre.next } ------------------------------------------ What does the fact Traces say? c. specify data domains ------------------------------------------ SPECIFY DATA AS SIGNATURES Want to model key data and objects Specify signatures with: with Add functions as needed for: - convenience - hiding modeling details Use the visualizer to check if sensible ------------------------------------------ d. specify security policy ------------------------------------------ SPECIFY THE SECURITY POLICY Specify the security policy as assertions Revise the sigs as needed ------------------------------------------ What happens when checking an assert in Alloy? e. specify dynamic operations as preds ------------------------------------------ SPECIFY DYNAMICS WITH PRED Specify a pred for each dynamic update for each sig (type of object) but not tied directly to events ------------------------------------------ f. describe messages and events containing them ------------------------------------------ DESCRIBE MESSAGES AND EVENTS Specify: - each kind of message (as a sig) - how each event affects objects (as a pred) ------------------------------------------ g. check security properties ------------------------------------------ CHECK SECURITY PROPERTIES See if there are counterexamples (attacks) Limit the events (and messages) to focus on particular attacks ------------------------------------------