Hack-Proof Drone, What is it?
Weapons Systems and Cyber Security
Who am I? 3
CyKoR @ DEFCON CTF 2015 (Advisor : Seungjoo Kim)
( 사 )HARU & SECUINSIDE (Founder & Board Member : Seungjoo Kim, 2011)
사이버무기시험평가연구센터 (CW-TEC)
Are Weapons Systems Secure? 8
Smart TV Hacking "Hackers to Target Smart TV Sets After Phones, Kaspersky Predicts", (Bloomberg, 2015) 9
Smart TV Hacking ( MBC Newsdesk) 10
Smart TV Hacking 11
Smart TV Hacking 12
Smart TV Hacking CIA and MI5 developed Weeping Angel to infect Samsung Smart TVs. 13
Smart TV Hacking Samsung Smart TVs have been sued by the CIA's hacking code. 14
Smart Car Hacking 15
Smart Car Hacking 16
Smart Car Hacking 17
Smart Car Hacking 18
Airplane (IFE) Hacking ( IOActive, In Flight Hacking System, December 20, 2016) 19
? 20
Left of Launch 21
Left of Launch 22 John Blackburn on Integrated Force Design: The Case of IMAD(Integrated Missile & Air Defence)
23
Left of Launch 24
Left of Launch 25
26
Recent suggestions that the fleet is vulnerable have sometimes been met with complacency and claims that the isolated 'air-gapped' systems cannot be penetrated. Whilst we recognise that it is important not to be alarmist, these claims are false. 27
Malware injection during manufacturing(a.k.a supply chain), mid-life refurbishment or software updates and data transmission interception allow potential adversaries to conduct long-term cyber operations. 28
Cybersecurity Test and Evaluation 29
30
Then... Ours? 31
사이버무기란? 사이버작전수행에직접운용되거나훈련용으로운용하는장비, 부품, 소프트웨어등으로서, 사이버영역의감시 정찰, 사이버작전지휘통제및능동적대응을위한장비 부품 소프트웨어또는사이버전훈련을위해운용되는모의공격체계, 모의훈련모델, 훈련용장비 시설등 ( 출처 : 국방사이버안보훈령 ) 32
다른말로, 사이버무기란? 네트워크와연결된모든무기체계 C4I 등의전술지휘자동화체계, 무인기 (UAV : Unmanned Aerial Vehicle) 및군위성통신체계, 위성전군방공경보체계, 해상작전위성통신체계등과같은통신체계, 그리고전술용전자식교환기, 야전용전화기, 휴대용 차량용 FM/AM 무전기등각종유 무선통신장비및연습훈련용 분석용 획득용워게임모델및전술훈련모의장비등이모두이에포함됨. ( 출처 : 국방사이버안보훈령의사이버무기체계세부분류 ) 33
34
Weapons Systems & Cyber Security 35
36
The key strategy is to upgrade weapon systems to qualify as High-Assurance Cyber Military Systems (HACMS), strategically designed to better withstand a cyber attack. 37
38
Hack-Proof Drones Possible with DARPA s HACMS(High Assurance Cyber Military Systems) Technology 39
40
Assurance (in a narrow sense) Robustness Strength Assurance 41
Assurance (in a broader sense) Physical Security Era Communication Security (COMSEC) Era Computer Security (COMPUSEC) Era (Early 1960s~) Information Security (INFOSEC) Era (1980s~) Information Assurance (IA) Era (1998 ~) Etc 42 : Operational Security (OPSEC)
Assurance (in a broader sense) The first standardized definition of IA was published in U.S. DoD Directive 5-3600.1 in 1996. The 1991 Gulf War has often been called the first information war. In many ways, the Gulf War was the harbinger of IA. 43
44
Communications are disrupted by hacking? 45
Communications are disrupted by dust storm?? 46
Assurance (in a broader sense) (Trustworthiness) Algirdas47 Avizienis, Jean-Claude Laprie, Brian Randell, and Carl Landwehr, Basic Concepts and Taxonomy of Dependable and Secure Computing, IEEE Transactions on Dependable and Secure Computing, VOL.1, NO.1, 2004.
Assurance (in a broader sense) Trustworthiness (or Dependability) is assurance that a system deserves to be trusted - that it will perform as expected despite environmental disruptions, human and operator error, hostile attacks, and design and implementation errors. Trustworthy systems reinforce the belief that they will continue to produce expected behaviour and will not be susceptible to subversion. 48 The "Trust in Cyberspace" report of the United States National Research Council
Assurance (in a broader sense) (Trustworthiness) Independent? No, Interdependent! Algirdas49 Avizienis, Jean-Claude Laprie, Brian Randell, and Carl Landwehr, Basic Concepts and Taxonomy of Dependable and Secure Computing, IEEE Transactions on Dependable and Secure Computing, VOL.1, NO.1, 2004.
Assurance (in a broader sense) 50
Assurance (in a broader sense) Security by Design to cope with complexity! 51
Assurance (in a broader sense) Embedded Security! 52
[Note] High-Confidence 53
[Note] High-Confidence 54
[Note] High-Confidence 55
[Note] High-Confidence 56
Security by Design (in a narrow sense) Considering security as early as the design phase of the software development process. 57 Michael Waidner, Michael Backes, Jörn Müller-Quade, "Development of Secure Software with Security By Design", Fraunhofer SIT Technical Reports, July 2014
Security by Design (in a broader sense) Systematically organized and methodically equipped framework that is applied over the lifecycle of secure software. (e.g.) Embedding of secure SW development at governance level, individual security processes for the SW's lifecycle phases, and security analyses of SW components integrated from other manufacturers. 58 Michael Waidner, Michael Backes, Jörn Müller-Quade, "Development of Secure Software with Security By Design", Fraunhofer SIT Technical Reports, July 2014
Security Engineering ( 보안공학 ) Security engineering is about building dependable (or trustworthy) embedded systems. (Trustworthiness) 59 Dependability is interchangeably used for trustworthiness (Sommerville, I.: "Software Engineering", Addison-Wesley, 6. edn., 2001, ISBN 0-201-39815-X)
Security Engineering ( 보안공학 ) Financial System High security + Medium reliability + No safety DB of Medical Records Medium security + Medium reliability + Medium safety Air Traffic Control System Medium security + High reliability + High safety Automobile Low (but now medium!) security + High reliability + High safety 60
Security Engineering 61
Our company has recruited a lot of hackers and done lots of pentesting, but we do not know if the quality of our product is really improving. 62
Our company has recruited a lot of hackers and done lots of pentesting, but we do not know if Can't the quality Guarantee of our Coverage! product is really improving. 63
Cryptography v.s Cryptanalysis Cryptology : science of secret communication Cryptography : design secret systems Cryptanalysis : break secret systems 64
Security Engineering ( 보안공학 ) Security Engineer : Like to fix systems. Security engineers are more intend on building robust security solutions (Firewalls, IDS, etc.). Similar Jobs : Information Assurance Engineer, Information Security Engineer, Information System Security Engineer Security Analyst : Try to break them. Security analysts are more concerned with probing for risks and weaknesses (Pentesting, Auditing, etc.). 65
Security Engineering ( 보안공학 ) 66
Security Engineering ( 보안공학 ) ( Paul Curran, Cyber Security Today: Career Paths, Salaries and In-Demand Job Titles, Aug 30, 2016) 67
5 Steps for Developing Dependable S/W 1. Define "goals" or "properties" (i.e., what you want the program to satisfy) 2. Design algorithms/protocols 3. Make standards 4. Generate source code 5. Compile to machine code (i.e., what actually runs) 68
69 "Cost Effective Use of Formal Methods in Verification and Validation"
Policy (= a set of requirements) Assurance Design Assurance Implementation/Operational Assurance Implementation/Operational Assurance 70 "Cost Effective Use of Formal Methods in Verification and Validation"
Policy (= a set of requirements) Assurance Design Assurance Chain of Evidence! Implementation/Operational Assurance Implementation/Operational Assurance 71 "Cost Effective Use of Formal Methods in Verification and Validation"
Policy (= a set of requirements) Assurance Design Assurance Then, don t need pentesting? Implementation/Operational Assurance Implementation/Operational Assurance 72 Daniel Jackson et al., "Software for Dependable Systems: Sufficient Evidence?"
Policy (= a set of requirements) Assurance Design Assurance Testing is indispensable, and no software system can be regarded as dependable if it has not been extensively tested, even if its correctness has been Implementation/Operational proven mathematically. Assurance Implementation/Operational Assurance 73 Daniel Jackson et al., "Software for Dependable Systems: Sufficient Evidence?"
Policy (= a set of requirements) Assurance Testing may find flaws that elude analysis Design because Assurance it exercises the system in its entirety, whereas analysis must typically make assumptions about the execution platform, the external environment, and Implementation/Operational operator responses, Assurance any of which may turn out to be unwarranted. Implementation/Operational Assurance 74 Daniel Jackson et al., "Software for Dependable Systems: Sufficient Evidence?"
Policy (= a set of requirements) Assurance At the same time, it is important to realize that Design Assurance testing alone is rarely sufficient to establish high levels of dependability. It is erroneous to believe that a rigorous development process, in which testing and code review are the only verification Implementation/Operational Assurance techniques used, justifies claims of extraordinarily high levels of dependability. Implementation/Operational Assurance 75 Daniel Jackson et al., "Software for Dependable Systems: Sufficient Evidence?"
Problems for STEP 1. 1. Define "goals" or "properties" (i.e., what you want the program to satisfy) How to identify and define goals correctly? By using Threat Modeling & Security Policy Modeling (SPM) 76
MS s STRIDE Threat Modeling Tools 77
LINDDUN Modeling 78
Other Methodologies and Tools TARA : Intel's Threat Agent Risk Assessment OWASP 79 https://www.owasp.org/index.php/application_t hreat_modeling WASC Threat Classification http://projects.webappsec.org/threat- Classification Trike http://octotrike.org ThreatModeler http://threatmodeler.com
80
Pentesting cannot replace threat modeling! Pentesting should be used as an adjunct to threat modeling. 81
82
83
84
Problems for STEP 2. 2. Design algorithms/protocols How to check if your algorithm or protocol satisfy the goals of STEP 1? By hand-proof or machine-checked proof 85
[Note] Why Design Assurance? Needham-Schroeder public-key authentication protocol (1978), which was believed secure for 17 years before Lowe discovered it was affected by a flaw such as replay attack (1995). 86
How to Get Design-Proof
[Note] Symbolic Analyses Originated from the seminal paper by Dolev and Yao (1983), and was developed mainly in the formal methods community Better automaton However, more complex to relate to real world security goals 88 Dolev D, Yao ACC (1983) On the security of public key protocols. IEEE Trans Inf Theory 29(2):198 208
[Note] Computational Analyses Originated from the papers by Goldwasser and Micali (1984) and by Yao (1982), and is based on more detailed computational models, involving complexity and probability theories Difficulty in proof automation But gives more realistic security assurance 89 Goldwasser S, Micali S (1984) Probabilistic encryption. J Comput Syst Sci 28(2):270 299 Yao AC (1982) Theory and application of trapdoor functions. In: 23rd FOCS, pp 80 91
How to Get Design-Proof Both symbolic and computational approaches provide rigorous proofs based on abstract models. A large gap still exists between these models and a real-world protocol implementation : Design << Implementation
[Note] Abstract Model 91 Aaron Tomb (Galois, Inc), "Assuring Crypto Code with Automated Reasoning", QCon, London, March 2017
[Note] Abstract Model Soundness : If the model is proved free from certain attacks under some assumptions, then the program is also free from the same attacks under some corresponding assumptions. 92 Aaron Tomb (Galois, Inc), "Assuring Crypto Code with Automated Reasoning", QCon, London, March 2017
How to Get Design-Proof Both symbolic and computational approaches provide rigorous proofs based on abstract models. Recently, some researchers have started investigating techniques that bring automated formal proofs closer to real implementations. (explain in later )
How to Get Design-Proof 94
How to Get Design-Proof 95
How to Get Design-Proof
Problems for STEP 3. 3. Make standards There might be specification mismatch between STEP 2 and STEP 3. We need equivalence proof to address the "gap" between the abstract algorithm/protocol and more concrete standard specification 97
Problems for STEP 4 ~ STEP5. 4. Generate source code and compile it into machine code Program might incorrectly implement the standard of STEP 3. Also, we can t be sure about the compiler! By using machine-checked proof tools such as Verified Software Toolchain. 98
[Note] Why Implementation Assurance? 99
How to Get Code-Proof 100
How to Get Code-Proof (in CGC case) 101
How to Get Code-Proof (in CGC case) 102 Symposium Celebrates Ed Clarke and Model Checking, CMU, September 2014
How to Get Code-Proof (in CGC case) 103 Symposium Celebrates Ed Clarke and Model Checking, CMU, September 2014
How to Get Code-Proof (in CGC case) 104 차상길, " 바이너리분석을통한자동익스플로잇생성 : 과거, 현재, 그리고미래 ", SECUINSIDE 2016
How to Get Code-Proof (in CGC case) 105 Symposium Celebrates Ed Clarke and Model Checking, CMU, September 2014
How to Get Code-Proof 106 Aaron Tomb (Galois, Inc), "Assuring Crypto Code with Automated Reasoning", QCon, London, March 2017
How to Get Code-Proof 107 ( Aaron Tomb, "Automated Verification of Real-World Cryptographic Implementations )
How to Get Code-Proof DES standard (e.g.) Cryptol, Z, etc. DES binary code Symbolic Execution (for constructing mathematical models of SW) (Reference Model) - Equivalence-checking - Safety-checking (e.g.) SAW with ABC (which uses SAT) Z3 (which uses SMT) Verified Software Toolkit (VST) 108 ( Aaron Tomb, "Automated Verification of Real-World Cryptographic Implementations )
How to Get Code-Proof Equivalence-Checking : Checks whether two functions, f and g, agree on all inputs Safety-Checking : Checks run-time exceptions. Given a function f, we would like to know if f's execution can perform operations such as division by zero or index out of bounds. David A. 109 Ramos and Dawson R. Engler, "Practical, Low-Effort Equivalence Verification of Real Code", CAV 2011 : This shows a technique for performing a semantic equivalence verification of new implementations vs reference implementations using a modified version of KLEE.
[Note] How to Link Model with Prog. 110 Matteo Avalle, Alfredo Pironti, Riccardo Sisto, "Formal Verification of Security Protocol Implementations: a Survey", Formal Aspects of Computing, January 2014.
[Note] The Limits of Automated Proof Several famous theorems (particularly Gödel s incompleteness theorem and Rice s theorem) imply that it s impossible to write a program that can always construct a proof of some arbitrary theorem (or some arbitrary property of a piece of software). Because of these theoretical limits, automated proof is no panacea. 111 In practice, however, cryptographic code contains characteristics that make many of its properties easier to prove.
Cryptol Haskell based DSL (Domain-Specific Language) for writing crypto-algorithms DSL : Programming language targeted at producing solutions in a given problem domain by enabling subject-matter experts to design solutions in terms they are familiar with and at a level of abstraction that makes most sense to them 112 Lewis JR, Martin B., "Cryptol: High-Assurance, Retargetable Crypto Development and Validation", MILCOM 2003
Cryptol Created by Galois Inc. with support from NSA Cryptol specifications can be used to verify various implementations C code, VHDL, etc. 113 Lewis JR, Martin B., "Cryptol: High-Assurance, Retargetable Crypto Development and Validation", MILCOM 2003
114
115 ( "Verified correctness and security of OpenSSL HMAC", Usenix Security Symposium 2015)
116
117
Assurance Levels 1. Define "goals" or "properties" (i.e., what you want the program to satisfy) In many cases, "provable security in cryptography" means only "design assurance"! i.e., the proposed algorithm/protocol satisfies certain security requirements 2. Design algorithms/protocols 3. Make standards 4. Generate source code 5. Compile to machine code (i.e., what actually runs) 118
Assurance Levels 1. Define "goals" or "properties" (i.e., what you want the program to satisfy) 2. Design algorithms/protocols 3. Make standards Common Criteria, even at EAL7, relies on testing (not mathematical proof!). There is no proof that security properties hold for the actual implementation (i.e., code proof). 4. Generate source code 5. Compile to machine code (i.e., what actually runs) 119
Assurance Levels 1. Define "goals" or "properties" (i.e., what you want the program to satisfy) 2. Design algorithms/protocols 3. Make standards 4. Generate source code We call this as High-Assurance (End-to-End Provably) Dependable Systems (e.g.) DARPA s HACMS(Hisg-Assurance Cyber Military Systems) Program, NICTA s sel4 Microkernel, etc 5. Compile to machine code (i.e., what actually runs) 120
NICTA s sel4 Microkernel 121
If It is Not Provable Mathematical proofs are best! But if it is not achievable, we should follow the well-defined software development processes!! (e.g.) Microsoft s SDL(Security Development Lifecycle) 122
If It is Not Provable 123
CC (Common Criteria) Evaluation
CC (Common Criteria) Evaluation
CC (Common Criteria) Evaluation 미국 Orange Book (TCSEC) 1985 캐나다 Canadian Criteria (CTCPEC) 1993 영국 독일 Green Books 1989 IT-Security Criteria 1989 U.S. Federal Criteria Draft 1993 European ITSEC (1991) v1.0 1996 v2.0 1998 v2.1 1999 v2.2 2004 v2.3 2005 v3.1 R1 2006.9 v3.1 R2 2007.9 프랑스 Blue-White-Red Book 1989 1999 년 : ISO/IEC 15408 국제표준으로제정 네덜란드 126 Netherlands Criteria 1989
CC (Common Criteria) Evaluation APE/ASE_OBJ APE/ASE_REQ 보안문제 보안목적 기능요구사항 ADV_FSP 기능명세 ADV_TDS ASE_TSS ADV_SPM 보안문제, 보안기능요구사항 (SFR) 과보안목적간일치성에대한요구사항을정의 A B A가 B에대응 ( 요구사항에따라 ) A B TOE 요약명세 정책모델 A 가 B 로상세화 TOE 요약명세에대한요구사항을정의 선택된 SFR 을정형화하여모델링하고, 이정형화된모델과기능명세간의일치성제공에대한요구사항정의 설계설명 ADV_IMP 구현표현 ALC_CMC.5 구현 127 ATE_AVA 기능명세모든, 설계, 분해구현에단계에서해당하는각표현을수행된기능요구사항에상호보완적인분석정의 구현시수행된기능시험및침투시험 시험클래스와취약성평가클래스에서시험된 TSF 가개발클래스의분해단계에서모두서술된사항임을검증
CC (Common Criteria) Evaluation Scope, Depth, Rigor High-Assurance Cyber System End-to- End Proof
CC (Common Criteria) Evaluation NSTISSP #11 Guidance IA & IA-Enabled Products Levels Of Robustness High robustness products EAL 7 6 5 IT Products and PP NSA Involvement in Product Evaluation NSA Evaluated Product List Crypto Modules and Algorithms Type 1 Crypto for Classified 4+ Medium robustness products Basic robustness products 129 4 3 2 1 0 NIAP - Certified CCTL Evaluations NIAP Labs Booz Allen Hamilton Cable & Wireless CoACT Criterian CSC Cygnacom InfoGard SAIC Level 1 Level 2 Level 3 Level 4 FIPS evaluated under CMVP (FIPS 140-1 or 140-2) Validated Product List http://csrc.nist.gov/cryptval CMVP Labs Atlan Cygnacom (CEAL) CoACT EWA Domus InfoGard
CC (Common Criteria) Evaluation 130
131
However Are provable secure schemes unbreakable? 132
Model Model does not cover all real 133 world attacks!
Reality Model does not cover all real 134 world attacks!
However Are provable secure schemes unbreakable? It depends on the threat model! 135
References 136
References 137
References 138
References 139
ICCC (International CC Conference)
ICMC (InternationalCryptoModuleConf)
Hack-Proof Drone, What is it?