




版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领
文档简介
1、VulnerabilitiesVulnerability Finding TodaySecurity bugs can bring $500-$100,000 on the open marketGood bug finders make $180-$250/hr consultingFew companies can find good people, many dont even realize this is possible.Still largely a black artSecurity Vulnerabilities What can Security bugs an attac
2、ker do? avoid authentication privilege escalation bypass security check deny service (crash/hose configuration) run code remotely Vulnerabilities Basis Concepts Techniques for Detecting Vulnerabilities Classification of Vulnerabilities Vulnerability AssessmentBasis Concepts6What Are Software Vulnera
3、bilities? A software vulnerability is an instance of a fault in the specification, development, or configuration of software such that its execution can violate the (implicit or explicit) security policy.Sources of Vulnerabilities Among the most frequently mentioned sources of security vulnerability
4、 problems in computer networks are design flaws incorrect implementation poor security management social engineering ExamplesVulnerability Distributions Across Operating SystemsLocations of observed vulnerabilities Majority of the vulnerabilities occurred in applications RedHat Linux (79%), Windows
5、2000 (77%) , and Solaris (90%) 10% to 20% of vulnerabilities are present in the underlying operating systems Example: Where is the Vulnerability ? int read_packet(int fd) char header50; char body100; size_t bound_a = 50; size_t bound_b = 100; read(fd, header, bound_b); read(fd, body, bound_b); retur
6、n 0; Example: Where is the bug? int read_packet(int fd) char header50; /model (header, 50) char body100; /model (body, 100) size_t bound_a = 50; size_t bound_b = 100; read(fd, header, 100); read(fd, body, 100); return 0; Example: Where is the bug? int read_packet(int fd) char header50; /model (heade
7、r, 50) char body100; /model (body, 100) size_t bound_a = 50; size_t bound_b = 100; read(fd, header, 100); /constant propagation read(fd, body, 100); /constant propagation return 0; Example: Where is the bug? int read_packet(int fd) char header50; /model (header, 50) char body100; /model (body, 100)
8、size_t bound_a = 50; size_t bound_b = 100; /check read(fd, dest.size = len) read(fd, header, 100); /constant propagation read(fd, body, 100); /constant propagation return 0; Example: Where is the bug? int read_packet(int fd) char header50; /model (header, 50) char body100; /model (body, 100) size_t
9、bound_a = 50; size_t bound_b = 100; /check read(fd, 50 = 100) = SIZE MISMATCH! read(fd, header, 100); /constant propagation read(fd, body, 100); /constant propagation return 0; Techniques for Detecting VulnerabilitiesTechniques for Detecting VulnerabilitiesSystem Verification Mathematically verifyin
10、g that a system satisfies certain constraintsCan prove the absence of vulnerabilitiesPenetration testing Start with system/environment characteristics Try to find vulnerabilitiesCan not prove the absence of vulnerabilitiesNotes Penetration testing is a testing technique, not a verification technique
11、 It can prove the presence of vulnerabilities, but not the absence of vulnerabilities For formal verification to prove absence, proof and preconditions must include all external factors Realistically, formal verification proves absence of flaws within a particular program, design, or environmentForm
12、al methodFormal method: automated technique based on mathematical logic used to analyze a property of a systemNational Security Agency was the major source of funding formal methods research and development in the 70s and early 80s Formal security models Tools for reasoning about security Applicatio
13、ns of using these tools to prove systems secureFMs are catching on“Formal methods can revolutionize development!”“Formal methods are difficult, expensive, not widely useful and for safety-critical systems only”People realize its importance Model checker Spin by Bell labs won System Software Award fo
14、r 2001 by the ACM Inventors of Model Checking (Edmund M.Clarke, E. Allen Emerson, and Joseph Sifakis) won ACM Turing Award for 2007 Intel, IBM, Motorola, etc. now employ hundreds of model checking experts Microsoft announced model checking project Zing IBM eServer p690 *, “ applied FV to some extent
15、 on approximately 40 design components and found more than 200 design flawsIt is estimated that 15% of these bugs were of extreme complexity and would have been difficult for traditional verification.Formal method The use of Internet brings security to the attention of masses What kind of problems c
16、an formal methods help to solve in security What problems will formal methods never help to solveThe Limits of Formal Methods Systems will never be 100% secure Formal methods will not break this axiom Assumptions about the systems environment Hard to state them explicitly The system could be deploye
17、d in an environment not originally designed Clever intruders find out how to violate these assumptions Security is not an either/or property Pay more, gain more e.g. Passwords, certificates, biometrics are measured in terms of degree of security for authenticationWhat Formal Methods Can Do Character
18、ize a systems behavior more precisely Define the systems desired properties precisely Prove a system meets its specification These capabilities of formal methods help practitioner in two ways Through specification, focusing on designers attention What is the interface What are the assumptions about
19、the system What is the system supposed to do under this condition and that condition What are the systems invariant properties Through verification Prove a system meets its security goals Find out the weaknesses of the systemHow They Can HelpFormal MethodsChecker/ProverSystem, MProperty, PNo,and why
20、YesMaybeSpecificationVerificationOne successful lightweight verification: Model CheckingNumerouslightweight speclanguagesSpecification Using a language with a mathematically defined syntax and semantics System properties Functional behavior Timing behavior Performance characteristics Internal struct
21、ureSpecification Specification has been most successful for behavioral properties Some other non-behavioral aspects of a system Performance Real-time constraints Security policies Architectural designSpecification Formal methods for specification of the sequential systems Z (Spivey 1988) Constructiv
22、e Z (Mirian 1997) VDM (Jones 1986) Larch (Guttag & Horning 1993) States are described in rich math structures (set, relation, function) Transition are described in terms of pre- and post- conditionsSpecification Formal methods for specification of the concurrent systems CSP (Hoare 1985) CCS (Milner
23、1980) Statecharts (Harel 1987) Temporal Logic (Pnueli 1981) I/O Automata (Lynch and Tuttle 1987) States range over simple domains, like integers Behavior is defined in terms of sequences, trees, partial orders of eventsExample:The Spec# Programming System The Spec# language: C# + non-null types, che
24、cked exceptions, method contracts, object invariants, The Spec# tool suite: A run-time checking compiler A static verifier: http:/ Spec# Codeclass Account int balance; Account(int initial) ensures balance = initial; balance = initial; void Deposit(int amount) modifies this.*; ensures balance = old(b
25、alance) + amount; balance = balance + amount; 31Verification Two well established approaches to verification Model Checking Theorem Proving Model checking Build a finite model of system and perform an exhaustive search Theorem Proving Mechanization of a logical proofModel Checking The technical chal
26、lenge is to devise an algorithm for handling large spacesScope of model checkersvLogic and functional design errors, especially related to concurrency and multi-threading:vDeadlock, livelock, starvation, blockingvRace conditionsvLocking and priority problemsvResource allocation errorsvReliance on re
27、lative speeds of execution of threadsvViolation of fixed system bounds (memory, stack, time)vSpecification incompleteness (unhandled event scenariosvSpecification redundancy (dead code)vLogic problems: missing causal or temporal relationsModel CheckingThere are two general approaches in model checki
28、ng1. Temporal Model Checking2. Model checking with a automaton specThe difference is between the specification First one : Temporal Logic Second one : AutomatonTemporal Model Checkingv Linear temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL,one can encode form
29、ulae describing events along a single computation path, such as:vThere is a condition, c, will eventually be truevc will be true until d becomes true v Computation tree logic (CTL) is a branching-time (modal) temporal logic, meaning that its model of time is a tree-like structure in which the future
30、 is not determined; there are different paths in the future, any one of which might be an actual path that is realised; some temporal operators quantify over paths that are possible from a given state for example:vthere is a path and c is true at all point on the pathvc is eventually true at some po
31、int on all paths Model Checking Model checking is completely automatic It produces counter examples The counter example usually represents subtle error in design The main disadvantage : state explosion problem!Theorem Proving Both the system and its desired properties are expressed in some mathemati
32、cal logic Theorem proving is the process of finding a proof from the axioms of the system It can be roughly classified Highly automated programs Interactive systems with special purpose capabilities In contrast to model checking, it can deal with infinite space Relies on techniques like reductionSys
33、tem Verification What are the problems? Invalid assumptions Limited view of system Still an inexact science External environmental factors Incorrect configuration, maintenance and operation of the program or systemWhat Is Penetration Testing? Testing the security of systems and architectures from a
34、hackers point of view A “simulated attack” with a predetermined goalTypes of TestingWhite Box Tester knows all information about system. Including source code, design, requirements. Most efficient technique. Avoids security through obscurity.Black Box Examines system as an outsider would. Tester bui
35、lds understanding of attack surface and system internals during test process. Can use to evaluate effort required to attack system. Helps test items that arent documented.Grey Box Apply both white box and black box techniques.Layering of Tests1. External attacker with no knowledge of systemLocate sy
36、stem, learn enough to be able to access it2. External attacker with access to systemCan log in, or access network serversOften try to expand level of access3. Internal attacker with access to systemTesters are authorized users with restricted accounts (like ordinary users)Typical goal is to gain una
37、uthorized privileges or informationFlaw Hypothesis Methodology1. Information gathering Become familiar with systems functioning2. Flaw hypothesis Draw on knowledge to hypothesize vulnerabilities3. Flaw testing Test them out4. Flaw generalization Generalize vulnerability to find others like itInforma
38、tion Gathering Devise model of system and/or components Look for discrepancies in components Consider interfaces among components Need to know system well (or learn quickly!) Design documents, manuals help Unclear specifications often misinterpreted, or interpreted differently by different people Lo
39、ok at how system manages privileged usersFlaw Hypothesizing Examine policies, procedures May be inconsistencies to exploit May be consistent, but inconsistent with design or implementation Examine implementations Use models of vulnerabilities to help locate potential problems Use manuals; try exceed
40、ing limits and restrictions; try omitting steps in proceduresFlaw Hypothesizing (cont) Identify structures, mechanisms controlling system Environment in which they work, and were built, may have introduced errors Throughout, draw on knowledge of other systems with similarities Which means they may h
41、ave similar vulnerabilities Result is list of possible flawsFlaw Testing Design test to be least intrusive as possible Must understand exactly why flaw might arise Procedure Back up system Verify system configured to allow exploit Take notes of requirements for detecting flaw Verify existence of fla
42、w May or may not require exploiting the flaw Make test as simple as possible, but success must be convincing Must be able to repeat test successfullyFlaw Generalization As tests succeed, classes of flaws emerge Sometimes two different flaws may combine for devastating attackFuzz Testing Automaticall
43、y generate test cases Many slightly anomalous test cases are input into a target interface Application is monitored for errors Inputs are generally either file based (.pdf, .png, .wav, .mpg) Or network based http, SNMP, SOAPTrivial ExampleStandard HTTP GET request GET /index.html HTTP/1.1Anomalous r
44、equests AAAAAA.AAAA /index.html HTTP/1.1 GET /index.html HTTP/1.1 GET %n%n%n%n%n%n.html HTTP/1.1 GET /AAAAAAAAAAAAA.html HTTP/1.1 GET /index.html HTTTTTTTTTTTTTP/1.1 GET /index.html HTTP/.Trivial Example Example: file fuzzing Create set of valid files. Choose parts of file to fuzz Meta
45、data: data format, size, etc. Content: bytes, HTML/XML tags, etc. Randomly modify parts of file. May need to recompute checksums. Submit fuzzed files to application. Monitor application for crashes and errors.Approach I: Black-box Fuzz Testing Given a program, simply feed it random inputs, see wheth
46、er it crashes Advantage: really easy Disadvantage: inefficient Input often requires structures, random inputs are likely to be malformed Inputs that would trigger a crash is a very small fraction, probability of getting lucky may be very lowEnhancement: Mutation-Based Fuzzing Take a well-formed inpu
47、t, randomly perturb (flipping bit, etc.) Little or no knowledge of the structure of the inputs is assumed Anomalies are added to existing valid inputs Examples: ZZUF, very successful at finding bugs in many real-world programs, /zzuf/ Taof, GPF, ProxyFuzz, FileFuzz, Filep, etc.FileF
48、uzzFileFuzz Identify TargetApplication vs. file type One file type multiple targetsVendor history Past vulnerabilitiesHigh risk targets Default file handlers Windows Explorer Windows Registry Commonly traded file types Media files Office documents Configuration filesIdentify targetIdentify inputsGen
49、erate fuzzed dataExecute fuzzed dataMonitor for exceptionsDetermine exploitabilityFileFuzz Identify InputsProprietary vs. open formats Vendor documents W GoogleBinary files e.g. images, video, audio, office documents, etc. Headers vs. dataText files e.g. *.ini, *.inf, *.xml Name/value pairs
50、Identify targetIdentify inputsGenerate fuzzed dataExecute fuzzed dataMonitor for exceptionsDetermine exploitabilityFileFuzz Generate Fuzzed Data Binary files Breadth FF FF FF FF 00 00 DB FE 0B 00 C5 00 00 01 E8 03 ; . D7 FF FF FF FF 00 DB FE 0B 00 C5 00 00 01 E8 03 ; . D7 CD FF FF FF FF DB FE 0B 00
51、C5 00 00 01 E8 03 ; . DepthD7 CD FD 9A 00 00 DB FE 0B 00 C5 00 00 01 E8 03 ; . D7 CD FE 9A 00 00 DB FE 0B 00 C5 00 00 01 E8 03 ; . D7 CD FF 9A 00 00 DB FE 0B 00 C5 00 00 01 E8 03 ; .Identify targetIdentify inputsGenerate fuzzed dataExecute fuzzed dataMonitor for exceptionsDetermine exploitabilityFil
52、eFuzz Execute Fuzzed DataCommand line arguments Windows explorer ToolsFolder OptionsFile TypesIdentify targetIdentify inputsGenerate fuzzed dataExecute fuzzed dataMonitor for exceptionsDetermine exploitabilityFileFuzz Monitor for ExceptionsVisual Error messages Blue screenEvent logs System logs Appl
53、ication logsDebuggersReturn codesDebugging APIIdentify targetIdentify inputsGenerate fuzzed dataExecute fuzzed dataMonitor for exceptionsDetermine exploitabilityFileFuzz Monitor for ExceptionsExecute Automated and repeatedMonitor Library - libdasm Capture Memory location Registry values Exception ty
54、pe Kill Set timeoutIdentify targetIdentify inputsGenerate fuzzed dataExecute fuzzed dataMonitor for exceptionsDetermine exploitability* crash.exe C:Program FilesWordPerfect Office 12ProgramsUA120.exe 2000 /qt c:fuzzast8.ast* Access Violation* Exception caught at 00403f06 mov eax,eax+edi*4* EAX:0014b
55、1b8 EBX:00000005 ECX:00435c00 EDX:0012fbac* ESI:00435c00 EDI:cccccccc ESP:0012fab8 EBP:0012fae8FileFuzz Determine ExploitabilitySkills Disassembly DebuggingVulnerability types Stack overflows Heap overflows Integer handling DoS Logic errors Format strings Race conditionsIdentify targetIdentify input
56、sGenerate fuzzed dataExecute fuzzed dataMonitor for exceptionsDetermine exploitabilityHow Much Fuzz Is Enough? Mutation based fuzzers may generate an infinite number of test cases. When has the fuzzer run long enough? Generation based fuzzers may generate a finite number of test cases. What happens
57、when theyre all run and no bugs are found?Code Coverage Some of the answers to these questions lie in code coverage Code coverage is a metric which can be used to determine how much code has been executed. Data can be obtained using a variety of profiling tools. e.g. gcovTypes of Code Coverage Line/
58、block coverage Measures how many lines of source code have been executed. Branch coverage Measures how many branches in code have been taken (conditional jmps) Path coverage Measures how many paths have been takenExample Requires 1 test case for line coverage 2 test cases for branch coverage 4 test
59、cases for path coverage i.e. (a,b) = (0,0), (3,0), (0,3), (3,3)Approach II: Constraint-basedAutomatic Test Case Generation Look inside the box Use the code itself to guide the fuzzing Assert security/safety properties Explore different program execution paths to check for security properties Challen
60、ge: 1. For a given path, need to check whether an input can trigger the bug, i.e., violate security property 2. Find inputs that will go down different program execution pathsRunning Examplef(unsigned int len)f(unsigned int len)unsigned int s; char unsigned int s; char * *buf;buf;if (len % 2=0) s =
温馨提示
- 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
- 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
- 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
- 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
- 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
- 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
- 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。
最新文档
- 家用纺织品的产品差异化与竞争优势考核试卷
- 智能车载设备的故障预测考核试卷
- 工艺美术品的商业模式创新考核试卷
- 专业技术培训引领行业变革考核试卷
- 家居装饰装修中的施工质量控制考核试卷
- 城市轨道交通的旅客负担与收入分析考核试卷
- 技术标准制定考核试卷
- 工业控制计算机在电力系统的应用考核试卷
- 学校租赁土地合同范本
- 公司并购签约合同范本
- 建设工程管理毕业论文
- 智慧水利建设顶层设计
- 数字示波器的工作原理及其应用
- 应聘登记表员工招聘登记表
- 肝内胆管结石治疗共识 课件
- 新一代智能变电站二次系统技术问答
- 索膜结构施工方案
- 常见婚姻家庭纠纷及调解的技巧课件
- 完整版老旧小区改造工程施工组织设计方案-3
- 从stahl精神药理学看二代抗精神病药物疗效及功课件
- 新人教版高中数学必修二全册教学课件ppt
评论
0/150
提交评论