I. Overview of Specification ------------------------------------------ SPECIFICATION Different levels: - Requirements - Detailed Design Overall Idea: 1. Description 2. Process for checking conformance Example: ------------------------------------------ II. Overview of UMLSec ------------------------------------------ UMLSec Overview Extension to Unified Modeling Language (UML) for specification of security in detailed designs Focuses on: - network security for systems - uses of cryptography Features: - Can specify some aspects of physical security - Tool support www-secse.cs.tu-dortmund.de/carisma/ Website: www-secse.cs.tu-dortmund.de/secse/pages/ research/UMLsec/index_en.shtml Book: Jan Jurjens. Secure Systems Development with UML. Springer-Verlag, Berlin, 2005. www.springer.com/us/book/9783540007012 ------------------------------------------ A. Problems Addressed ------------------------------------------ WHY SYSTEM/PROTOCOL DESIGN? Need an overview of the detailed design - check against requirements - see how components compose Deadly Sin #21: - Using Cryptography Incorrectly esp. creating your own protocol Shamir (1999): strong crypto doesn't matter, if it is used incorrectly or if the system has other weaknesses However: ------------------------------------------ Why not just build a system and try penetration testing? B. approach ------------------------------------------ GOALS AND APPROACH Goal: tool for - formal specification and - automated verification of detailed designs at component level Approach: - model both the system and - model makes various assumptions such as: - encrypted data cannot be decrypted - certain links are secure - what an attacker can do - specify security properties at a high level with UML stereotypes e.g., <>, > - specify constraints (in OCL) - can generate code or tests from model ------------------------------------------ Can one do verification based on informal design documents? Why specify detailed designs? C. elements of UMLSec 1. stereotypes ------------------------------------------ STEREOTYPES Drawn from a list (p. 51) Label parts of UML diagrams Add security-specific information: - assumptions about physical system <>, <>, <> - security requirements about structure <> or about data values <> - security policies <>, <> ------------------------------------------ 2. physical security using deployment diagrams ------------------------------------------ DEPLOYMENT DIAGRAMS FOR CONTEXT AND PHYSICAL SECURITY Goal: describe how system parts fit together for operation and maintenance Shows: processing nodes (boxes) and components that run on them, and connections Nodes are shown as "perspective cubes" with software deployed inside them ------------------------------------------ What are these like? 3. cryptographic techniques a. symmetric and asymmetric cryptography Is this review from CIS 3360? ------------------------------------------ SYMMETRIC CRYPTOGRAPHY Uses a single secret key both to encrypt and decrypt messages Advantages: + can be fast Disadvantages: - both parties must know the key Examples: AES ------------------------------------------ ------------------------------------------ PUBLIC KEY CRYPTOGRAPHY Based on hard to compute problems: - integer factorization - etc. Uses 2 keys, each can be used to Keys play different roles: public key (K): -1 private key (K ): ------------------------------------------ How can we use this to send messages securely? How does signing work? b. notations ------------------------------------------ Cryptographic Expressions from: R. Needham and M. Schroeder. "Using encryption for authentication in large networks of computers." CACM 21(12):993-999, Dec. 1978. Notation: K is a cryptographic key K is a I -1 K is a I {M} is message M K Ext (X) is K Sign (M) is message M K M1::M2 is message M1 ------------------------------------------ 4. statechart diagrams ------------------------------------------ STATECHART DIAGRAMS for state-based control of objects or components Rounded rectanges represent Arrows represent labeled with event[guard]/action events are operation calls or returns guards are boolean expressions actions may be call() or send() solid circle representing circle with solid circle inside representing ------------------------------------------ ------------------------------------------ EXAMPLE STATECHART DIAGRAM For the router: ------------------------------------------ 5. sequence diagrams ------------------------------------------ SEQUENCE DIAGRAMS Boxes representing Vertical thin boxes repesent Arrows repesent Example: ------------------------------------------ a. activity diagrams ------------------------------------------ ACTIVITY DIAGRAMS Special cases of statecharts that specify Example ------------------------------------------ D. UML Machine semantics ------------------------------------------ EXECUTION MODEL Components communicate by links, from the deployment diagram. Components modeled by functions that follow the specification, each has an input queue of messages and an output queue of messages, both of which are connected to links Links modeled by queues of messages Behavior of specification S, [[S]] 0. Deliver some messages in link queues to input queues. 1. Select some messages in input queues, of components C_i, these are the input events for the C_i. 2. Have the selected components, C_i, each process the input events as each C_i has specified 3. Place any outputs on the corresponding link queues 4. Adversary can delete/modify/insert messages in link queues, according to its capabilities. ------------------------------------------ ------------------------------------------ BEHAVIOR AND REFINEMENT def: A UML machine is a UML specification def: A *behavior of a UML machine* is Can there be several possible behaviors? When does a machine, T, refine a given S? def: T is a delayed refinement of S if ------------------------------------------ Why can't T have more behaviors? Why can T have fewer behaviors? Why do we care about refinement? E. modeling adversaries ------------------------------------------ MODELING ADVERSARIES In general, can give a UML specification for some specific behavior. Normally based on abstract threats: which are actions on messages (in links) and which is an action on a node. State of an adversary is its knowledge, K A ------------------------------------------ ------------------------------------------ MOST GENERAL ADVERSARY MACHINE An adversary of the given type that has the most nondeterminism ------------------------------------------ Why is the most nondeterminism intersting? Why is that such an adversary intersting? F. stereotypical security properties 1. secrecy ------------------------------------------ <> A system S preserves the secrecy of data d against an adversary of type A if Example: S preserves secrecy of a message m if it only sends out {m} K and keeps K secret. ------------------------------------------ What about a system S that receives a session key K encrypted with S's public key, and then sends {m} encrypted with K? 2. integrity ------------------------------------------ <> def: Let E be a set of acceptable values for a variable v. Then a system S *preserves the integrity of v* if ------------------------------------------ 3. authenticity ------------------------------------------ <> Idea: track the origin of all data = component which first produced it def: A system S *preserves authenticity of v* if the origin of v's value is ------------------------------------------ If we have authenticity of messages, do we also have integrity? When does integrity imply authenticity? 4. freshness ------------------------------------------ FRESH def: Let D be a subsystem instance or object. Then an atomic value *d is fresh in D* if if d only appears in the overall diagram in D. ------------------------------------------ III. Modeling and Analysis with UMLSec A. Transport Layer Security (TLS) B. CEPS purchase transaction C. Airline Reservation System Example What could be the exchange between the client and the router? What can be done now that the client and server have exchanged keys?