Summary of the NSF/IARPA/NSA Workshop on the Science of Security

Summary of the NSF/IARPA/NSA Workshop on the Science of Security

Summary of the NSF/IARPA/NSA Workshop on the Science of Security David Evans University of Virginia INFOSEC Research Council 16 July 2009 Outline Workshop description, participants, format Summary of prevailing consensus Highlight some key ideas

What next? Workshop Stated Goals: Identify scientific questions regarding computer security Stimulate new work toward defining and answering those questions. Encourage work that goes beyond ad hoc point solutions and informal security arguments to discover foundational scientific laws for reasoning about and designing secure computing systems. 2-day workshop in Berkeley, CA (Nov 2008) Premise: need new ideas from outside traditional infosec research community 44 Participants David Bray, IDA Fred Chang, U. of Texas/NSA

Byron Cook, MSR/Cambridge Son Dao, HRL Laboratories Anupam Datta, CMU John Doyle, Caltech Anthony Ephremides, UMd David Evans (organizer), UVa Manfai Fong, IARPA Stephanie Forrest, UNM John Frink, ODUSD Joshua Guttman, MITRE Robert Herklotz, AFOSR Alfred Hero, U. of Michigan Sampath Kannan, NSF Steven King, ODUSD Carl Landwehr, IARPA Greg Larsen, IDA Karl Levitt (organizer), NSF Brad Martin (organizer), NSA

John Mallery, MIT CSAIL Roy Maxion, CMU Robert Meushaw, NSA John Mitchell, Stanford Pierre Moulin, U. Illinois Timothy Murphy, IARPA Dusko Pavlovic, Kestrel/Oxford Nick Petroni, IDA Lisa Porter, IARPA Michael Reiter, UNC Phillip Rogaway, UC Davis John Rushby, SRI Stuart Russell, UC Berkeley Fred Schneider, Cornell Jim Silk (organizer), IDA Dawn Song, UC Berkeley Pieter Swart, Los Alamos NL

Vicraj Thomas, BBN/GENI Hal Varian, Berkeley/Google Cliff Wang, ARO Rebecca Wright, Rutgers Shouhuai Xu, UT San Antonio Ty Znati, NSF Lenore Zuck, NSF Participant Affiliation David Bray, IDA Fred Chang, U. of Texas/NSA Byron Cook, MSR/Cambridge Son Dao, HRL Laboratories Anupam Datta, CMU John Doyle, Caltech Anthony Ephremides, UMd David Evans (organizer), UVa Manfai Fong, IARPA Stephanie Forrest, UNM

John Frink, ODUSD Joshua Guttman, MITRE Robert Herklotz, AFOSR Alfred Hero, U. of Michigan Sampath Kannan, NSF Steven King, ODUSD Carl Landwehr, IARPA Greg Larsen, IDA Karl Levitt (organizer), NSF Brad Martin (organizer), NSA John Mallery, MIT CSAIL Roy Maxion, CMU Robert Meushaw, NSA John Mitchell, Stanford Pierre Moulin, U. Illinois Timothy Murphy, IARPA Dusko Pavlovic, Kestrel/Oxford

Nick Petroni, IDA Lisa Porter, IARPA Michael Reiter, UNC Phillip Rogaway, UC Davis John Rushby, SRI Stuart Russell, UC Berkeley Fred Schneider, Cornell Jim Silk (organizer), IDA Dawn Song, UC Berkeley Pieter Swart, Los Alamos NL Vicraj Thomas, BBN/GENI Hal Varian, Berkeley/Google Cliff Wang, ARO Rebecca Wright, Rutgers Shouhuai Xu, UT San Antonio Ty Znati, NSF Lenore Zuck, NSF 14 Government

9 Governmentish 21 Academia Participant Background David Bray, IDA Fred Chang, U. of Texas/NSA Byron Cook, MSR/Cambridge Son Dao, HRL Laboratories Anupam Datta, CMU John Doyle, Caltech Anthony Ephremides, UMd David Evans (organizer), UVa Manfai Fong, IARPA Stephanie Forrest, UNM John Frink, ODUSD Joshua Guttman, MITRE Robert Herklotz, AFOSR Alfred Hero, U. of Michigan Sampath Kannan, NSF

Steven King, ODUSD Carl Landwehr, IARPA Greg Larsen, IDA Karl Levitt (organizer), NSF Brad Martin (organizer), NSA John Mallery, MIT CSAIL Roy Maxion, CMU Robert Meushaw, NSA John Mitchell, Stanford Pierre Moulin, U. Illinois Timothy Murphy, IARPA Dusko Pavlovic, Kestrel/Oxford Nick Petroni, IDA Lisa Porter, IARPA Michael Reiter, UNC Phillip Rogaway, UC Davis John Rushby, SRI

Stuart Russell, UC Berkeley Fred Schneider, Cornell Jim Silk (organizer), IDA Dawn Song, UC Berkeley Pieter Swart, Los Alamos NL Vicraj Thomas, BBN/GENI Hal Varian, Berkeley/Google Cliff Wang, ARO Rebecca Wright, Rutgers Shouhuai Xu, UT San Antonio Ty Znati, NSF Lenore Zuck, NSF Traditional Infosec Researchers Computer Scientists Outside Area Format

2 days Keynotes: Fred Schneider, Frederick Chang Panels: What is a science of security? What can we learn from other fields? How can we reason about impossible things? Are scientific experiments in security possible? Breakout groups on various topics including: Metrics, provable security, managing complexity, composition, experimentation Philosophical Questions (Usually Not Worth Discussing) Is there science in computer system security? Yes, but of course there should be more.

Meaning of Science Systematization of Knowledge Ad hoc point solutions vs. general understanding Repeating failures of the past with each new platform, type of vulnerability Scientific Method Process of hypothesis testing and experiments Building abstractions and models, theorems Universal Laws Widely applicable Make strong, quantitative predictions Realistic Goal Can we be a science like physics or chemistry? Unlikely humans will always be a factor in security. How far can we get without modeling humans?

How far can we get with simple models of human capabilities and behavior? Workshop charge: avoid human behavior issues as much as possible. Alchemy (700-~1660) Well-defined, testable goal (turn lead into gold) Established theory (four elements: earth, fire, water, air) Methodical experiments and lab techniques (Jabir ibn Hayyan in 8th century) Wrong and unsuccessful...but led to modern chemistry. Questions for a Science of Security Resilience: Given a system P and an attack

class A, is there a way to: Prove that P is not vulnerable to any attack in A? Construct a system P' that behaves similarly to P except is not vulnerable to any attack in A? How can we determine if a system A is more secure than system f(A) (where f is some function that transforms an input program or system definition)? Metrics Scientific understanding requires quantification For most interesting security properties, not clear what to measure or how to measure it Comparative metrics may be more useful/feasible than absolute metrics: How can we quantify the security of two systems A and B in a way that establishes which is more secure for a given context? Quantify the security of a system A and a system f(A) (where f

is some function that transforms an input program or system definition)? Metrics: Promising Approaches Experimental metrics: more systematic red team approaches (hard to account for attacker creativity) Economic metrics: active research community Epidemiological metrics: good at modeling spread over network, but need assumptions about vulnerabilities Computational complexity metrics: define attacker search space (promising for automated diversity) Formal Methods and Security Lots of progress in reasoning about correctness properties Byron Cook: reasoning about termination and liveness

Systems fail when attackers find ways to violate assumptions used in proof Need formal methods that make assumptions explicit in a useful way Combining formal methods with enforcement mechanisms that enforce assumption Formal Methods Questions Refinement: Can we use refinement approaches (design ... implementation) that preserve security properties the way they are used to preserve correctness properties now? Program analysis: What security properties can be established by dynamic and static analysis? How can computability limits be overcome using hybrid analysis, system architectures, or restricted programming languages? Experimentation

Security experiments require adversary models Need to improve adversary models Coalesce knowledge of real adversaries Canonical attacker models (c.f., crypto) Design for reproducibility Roy Maxion later today Some Highlights Caveat: I wont do justice to these ideas...but (almost) all the presentation materials are here: http://sos.cs.virginia.edu/agenda.html Towards Scientific Defenses Due to Fred Schneider Target for 2015: Defense class D enforces

policy class P when facing attacks from class A. Defining classes of policies: System behavior: infinite trace of states (or events) t = s0 s1 s2 ... si ... System property: set of traces P = { t | pred(t) } A system S satisfies property P if S P Formal way to reason about what system properties different mechanisms can enforce Example: Execution Monitoring Due to Fred Schneider Ideal reference monitor: sees all policy-relevant events, cannot be circumvented, can block execution immediately EM-enforceable policies Safety Properties Implementation approaches: Inlined reference monitor (SASI, Naccio)

Proof-carrying code: prove the automaton necessary to enforce policy is correctly embedded in program Combine approaches for improved performance and small TCB Limitations of Execution Monitoring Due to Fred Schneider Liveness properties: something good eventually happens Requires reasoning about all possible future paths Non-interference: low-level users get same outputs regardless of high-level actions Requires reasoning about all possible executions Hyper-Properties Clarkson & Schneider, 2008

Hyper-property: set of sets of traces System satisfies HP is set of traces it can produce is in the HP set Claim: can define all security properties as Hyperproperties Open questions: Is there a way to enforce/verify them? Are there restricted property classes between EMenforceable and Hyper-properties? k-safety hyperproperties: property that can be refuted by observing k traces (Loosely) Due to Fred Chang Formal Methods vs. Complexity Complexity Pessimists View Deployed Systems

Formal Techniques Capability 2009 Time 2050 (Loosely) Due to Fred Chang Formal Methods vs. Complexity Complexity Optimists View Deployed Systems TCB of Deployed

Formal Techniques Capability 2009 Time 2050 Ideas from Networks and Biological Systems Due to John Doyle Bowtie architecture in: Internet Applications TCP/IP Link Power distribution Diverse function Power plants Stan Many Devices

Biological Systems Cell Metabolism (next slide) Universal Control Diverse components Constraints that De-Constrain Hu Var ge iety Precursors Catabolism

Nutrients Taxis and transport Same 12 in all Core metabolism cells John Doyles slide rs a g Su cids A

o n i Am Nucleotides Fatty ac i ds Cofac tors Carriers Same 8 in all cells 0

0 1 e am l s s l a in n is m a g or Robustness/Fragility Tradeoff Due to John Doyle Systems tradeoff robustness and fragility: Robustness for some set of

permutations implies fragility for other set of permutations Some fragilities are inevitable for complex systems Seems to hold for biological evolved systems, must it for engineered systems? Fragile Robust Recap Summary Systematization of Knowledge Valuable Ad hoc pointand solutions vs. general understanding achievable:

need the right Repeating failures of the past with each new platform, type of incentives for community vulnerability Scientific Method Progress Process of hypothesis and experiments in usefultesting models; big challenges constructing Building abstractions and models, theorems security experiments

in Universal Laws Uncertainty Widely applicable if such laws exist; long go Make quantitativequantification. predictions forstrong, meaningful way to What Next?: Systematization of Knowledge IEEE Symposium on Security and Privacy

(Oakland 2010): call for systematization papers The goal of this call is to encourage work that evaluates, systematizes, and contextualizes existing knowledge. These papers will provide a high value to our community but would otherwise not be accepted because they lack novel research contributions. Discussion What next? Metrics Experimentation Formal methods Challenge problems?

Recently Viewed Presentations

  • PowerPoint 簡報 - Hanna Lind

    PowerPoint 簡報 - Hanna Lind

    TXC Confidential & Proprietary | Thickness of Blank: Determines Frequency. A. l. AT Cut Crystal - Resonance frequency is determined by thickness of blank.
  • Rensselaers Sustainability Charrette Environment  Economics  Education Envision  Explore

    Rensselaers Sustainability Charrette Environment Economics Education Envision Explore

    Operations - Defined. Operations at Rensselaer involves all day to day activities that impact the learning and living environment of Rensselaer students, faculty, and staff. Specific areas include building maintenance and cleaning, upkeep of lawn and garden areas, operation of...
  • ITU Guidelines on Digital Broadcasting An overview Workshop

    ITU Guidelines on Digital Broadcasting An overview Workshop

    System Parameters 4.5/5.5 Radiation Characteristics 4.7/5.7 Shared & Common Design Principles 4.9 Network Rollout Planning 4.6. ... Trebuchet MS Arial Verdana Wingdings Zurich BT Times New Roman Univers Calibri Courier New NGN Impact Pacific 1_NGN Impact Pacific ITU Guidelines on...
  • Jennifer Togyer SJAM Co-op Office Manager Favorite Memory:

    Jennifer Togyer SJAM Co-op Office Manager Favorite Memory:

    McMaster University, Engineering Department. Favorite memory. My favorite memory was Monday November 1st when I presented in front of very important people from Union Gas company, McMaster University, and University of Windsor. ... Cathy Weaver and SJAM Music Department. Favourite.
  • Lady Di - Webnode

    Lady Di - Webnode

    Goodbye England's Rose, From a country lost without your soul, Who'll miss the wings of your compassion More than you'll ever know. Sbohem Anglická růže, ze země ztracené bez Tvé duše, které budou chybět křídla Tvého soucitu, víc, než bys...
  • Light Induced Dehalogenation of Halobenzene using Carbon Dots

    Light Induced Dehalogenation of Halobenzene using Carbon Dots

    Light Induced Dehalogenation of Halobenzene using Carbon DotsAnthony J. Lemieux, Christine A. CaputoDepartment of Chemistry, University of New Hampshire, Durham, NH 03824. Carbon Dots (CDs) are fluorescent nanoparticles that consist of a graphitic carbon core with a passivated surface and...
  • LE F I T C N O J

    LE F I T C N O J

    Soyonssérieux 2 minutes et regardons la conjugaison des verbesréguliers au subjonctif. Formation du subjonctif. La formation du subjonctifprésentestsimilaire pour tous les verbesréguliers (-ER, -IR, -RE). Prenez la forme de la troisièmepersonneplurielle (ils) au présent de l'indicatif et ...
  • Why did the Cold War spread to Asia?

    Why did the Cold War spread to Asia?

    The 'anti-Red' crusade shifted public opinion against Communism in America. McCarthy began to accuse everyone of being Communists, including members of the US Army and State Department. He even claimed that the Truman administration was influenced by Communism, it was...