網(wǎng)絡(luò)攻擊與防范3-漏洞

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