版權(quán)說明:本文檔由用戶提供并上傳,收益歸屬內(nèi)容提供方,若內(nèi)容存在侵權(quán),請進(jìn)行舉報(bào)或認(rèn)領(lǐng)
文檔簡介
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、ng Temporal Model Checking 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 formulae
29、 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 is
30、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 point
31、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 mathematical
32、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 reductionSystem
33、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 hack
34、ers 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 builds
35、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 TestsExternal attacker with no knowledge of systemLocate system, l
36、earn enough to be able to access itExternal attacker with access to systemCan log in, or access network serversOften try to expand level of accessInternal attacker with access to systemTesters are authorized users with restricted accounts (like ordinary users)Typical goal is to gain unauthorized pri
37、vileges or informationFlaw Hypothesis MethodologyInformation gathering Become familiar with systems functioningFlaw hypothesis Draw on knowledge to hypothesize vulnerabilitiesFlaw testing Test them outFlaw generalization Generalize vulnerability to find others like itInformation Gathering Devise mod
38、el 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 Look at how system manages
39、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 exceeding limits and restrictio
40、ns; 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 have similar vulnerabiliti
41、es 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 flaw May or may not require
42、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 Automatically generate test cases Man
43、y 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 requests AAAAAA.AAAA /inde
44、x.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 Metadata: data format, size,
45、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 whether it crashes Advantage:
46、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 input, randomly perturb (flip
47、ping 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.FileFuzzFileFuzz Identify Targ
48、etApplication 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 inputsGenerate fuzzed dataExecute
49、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 pairsIdentify targetIdentify i
50、nputsGenerate 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 C5 00 00 01 E8 03 ; . Dep
51、thD7 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 exploitabilityFileFuzz Execute Fuzzed Data
52、Command 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 Application logsDebuggersRetu
53、rn 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 type Kill Set timeoutIdenti
54、fy 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:0014b1b8 EBX:00000005 ECX:0043
55、5c00 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 inputsGenerate fuzzed dataExec
56、ute 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 when theyre all run and n
57、o 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/block coverage Measures h
58、ow 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 cases for path coverage i
59、.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 Challenge: 1. For a given path,
60、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 = len;if (len % 2=0) s = le
溫馨提示
- 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
- 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權(quán)益歸上傳用戶所有。
- 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁內(nèi)容里面會(huì)有圖紙預(yù)覽,若沒有圖紙預(yù)覽就沒有圖紙。
- 4. 未經(jīng)權(quán)益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
- 5. 人人文庫網(wǎng)僅提供信息存儲(chǔ)空間,僅對用戶上傳內(nèi)容的表現(xiàn)方式做保護(hù)處理,對用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對任何下載內(nèi)容負(fù)責(zé)。
- 6. 下載文件中如有侵權(quán)或不適當(dāng)內(nèi)容,請與我們聯(lián)系,我們立即糾正。
- 7. 本站不保證下載資源的準(zhǔn)確性、安全性和完整性, 同時(shí)也不承擔(dān)用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。
最新文檔
- 引流提成合同模板
- 工地設(shè)備看護(hù)合同模板
- 校園收購合同模板
- 軟件設(shè)備安裝合同模板
- 課時(shí)04流體壓強(qiáng)與流速的關(guān)系(重點(diǎn)練)-2024-2025學(xué)年八年級物理下冊十分鐘同步課堂專練(人教版)含答案
- 遠(yuǎn)方物流合同模板
- 油畫借用合同模板
- 單價(jià)合同范本(2篇)
- 車輛抵欠款合同范本(2篇)
- 淮安市房產(chǎn)出售合同模板
- 物業(yè)保盤行動(dòng)策劃方案
- 資產(chǎn)盤點(diǎn)合同范本
- 解放碑商圈報(bào)告
- 胃殘余量測量護(hù)理課件
- 《人血白蛋白》課件
- 裝修工程監(jiān)理方案投標(biāo)方案技術(shù)標(biāo)
- 《復(fù)活》 統(tǒng)編版高中語文選擇性必修上冊
- 宮腔鏡手術(shù)配合護(hù)理查房
- 生產(chǎn)異常管理及分析
- XX元器件選用報(bào)告
- 江西省南昌二十八中教育集團(tuán)2023-2024學(xué)年九年級上學(xué)期期中英語試卷+
評論
0/150
提交評論