Slide 1MenuProblem Classes if P NP:Halting ProblemInformal ProofProof by Contradiction“Evaluates to 3” ProblemUndecidability ProofHello-World? ProblemSlide 10Slide 11From Paul Graham’s “Undergraduation”:Morris Internet Worm (1988)Worm Detection ProblemSlide 15Conclusion?“Solving” Undecidable ProblemsActual is-virus? ProgramsProof RecapHow convincing is our Halting Problem proof?ChargeDavid Evanshttp://www.cs.virginia.edu/evansCS150: Computer ScienceUniversity of VirginiaComputer ScienceClass 25: Undecidable ProblemsInfluenza Virus2CS150 Fall 2005: Lecture 25: Undecidable ProblemsMenu•Review: –Undecidability–Halting Problem•How do we prove a problem is undecidable?•What do we do when faced with an undecidable problem?3CS150 Fall 2005: Lecture 25: Undecidable ProblemsProblem Classes if P NP:Simulating Universe: O(n3)SmileysFind Best: (n)NP-CompleteP(n)NP3SATDecidableUndecidablefind proofhalts?4CS150 Fall 2005: Lecture 25: Undecidable ProblemsHalting ProblemDefine a procedure halts? that takes a procedure and an input evaluates to #t if the procedure would terminate on that input, and to #f if would not terminate.(define (halts? procedure input) … )5CS150 Fall 2005: Lecture 25: Undecidable ProblemsInformal Proof (define (contradict-halts x) (if (halts? contradict-halts null) (loop-forever) #t))If contradict-halts halts, the if test is true and it evaluates to (loop-forever) - it doesn’t halt!If contradict-halts doesn’t halt, the if test if false,and it evaluates to #t. It halts!6CS150 Fall 2005: Lecture 25: Undecidable ProblemsProof by Contradiction1. Show X is nonsensical.2. Show that if you have A and B you can make X.3. Show that you can make A.4. Therefore, B must not exist.X = contradict-haltsA = a Scheme interpreter that follows the evaluation rulesB = halts?7CS150 Fall 2005: Lecture 25: Undecidable Problems“Evaluates to 3” ProblemInput: A procedure P and input IOutput: true if evaluating (P I ) would result in 3; false otherwise. Is “Evaluates to 3” decidable?8CS150 Fall 2005: Lecture 25: Undecidable ProblemsUndecidability ProofSuppose we could define evaluates-to-3? that decides it. Then we could define halts?:(define (halts? P I) (if (evaluates-to-3? ‘(begin (P I) 3)) #t #f))Since it evaluates to 3, we know (P I) must halt.The only way it could not evaluate to 3, is if (P I)doesn’t halt. (Note: assumes (P I) cannot produce an error.)9CS150 Fall 2005: Lecture 25: Undecidable ProblemsHello-World? ProblemInput: A procedure P and input IOutput: true if evaluating (P I ) would print out “Hello World!”; false otherwise. Is Hello-World? decidable?10CS150 Fall 2005: Lecture 25: Undecidable ProblemsUndecidability ProofSuppose we could define hello-world? that decides it. Then we could define halts?:(define (halts? P I) (if (hello-world? ‘(begin ((remove-prints P) I) (print “Hello World!”)) #t #f))11CS150 Fall 2005: Lecture 25: Undecidable ProblemsProof by Contradiction1. Show X is nonsensical.2. Show that if you have A and B you can make X.3. Show that you can make A.4. Therefore, B must not exist.X = halts?A = a Scheme interpreter that follows the evaluation rulesB = hello-world?12CS150 Fall 2005: Lecture 25: Undecidable ProblemsFrom Paul Graham’s “Undergraduation”:My friend Robert learned a lot by writing network software when he was an undergrad. One of his projects was to connect Harvard to the Arpanet; it had been one of the original nodes, but by 1984 the connection had died. Not only was this work not for a class, but because he spent all his time on it and neglected his studies, he was kicked out of school for a year. ... When Robert got kicked out of grad school for writing the Internet worm of 1988, I envied him enormously for finding a way out without the stigma of failure. ... It all evened out in the end, and now he’s a professor at MIT. But you’ll probably be happier if you don’t go to that extreme; it caused him a lot of worry at the time. 3 years of probation, 400 hours of community service, $10,000+ fine13CS150 Fall 2005: Lecture 25: Undecidable ProblemsMorris Internet Worm (1988)•P = fingerd –Program used to query user status–Worm also attacked other programs•I = “nop400 pushl $68732f pushl $6e69622f movl sp,r10 pushl $0 pushl $0 pushl r10 pushl $3 movl sp,ap chmk $3b”(is-worm? P I) should evaluate to #t•Worm infected several thousand computers (~10% of Internet in 1988)14CS150 Fall 2005: Lecture 25: Undecidable ProblemsWorm Detection ProblemInput: A program P and input IOutput: true if evaluating (P I) would cause a remote computer to be “infected”.Virus Detection ProblemInput: A program P and input IOutput: true if evaluating (P I) would cause a file on the host computer to be “infected”.15CS150 Fall 2005: Lecture 25: Undecidable ProblemsUndecidability ProofSuppose we could define is-worm? Then:(define (halts? P I) (if (is-worm? ‘(begin ((deworm P) I) worm-code)) #t #f))Since it is a worm, we know worm-code was evaluated, and P must halt.The worm-code would not evaluate, so P must not halt.Can we make deworm ?16CS150 Fall 2005: Lecture 25: Undecidable ProblemsConclusion?•Anti-Virus programs cannot exist!“The Art of Computer Virus Research and Defense”Peter Szor, Symantec17CS150 Fall 2005: Lecture 25: Undecidable Problems“Solving” Undecidable Problems•No perfect solution exists:–Undecidable means there is no procedure that:1. Always gives the correct answer2. Always terminates•Must give up one of these to “solve” undecidable problems–Giving up #2 is not acceptable in most cases–Must give up #118CS150 Fall 2005: Lecture 25: Undecidable ProblemsActual is-virus? Programs•Give the wrong answer sometimes–“False positive”: say P is a virus when it isn’t–“False negative”: say P is safe when it is•Database of known viruses: if P matches one of these, it is a virus•Clever virus authors can make viruses that change each time they propagate–A/V software ~ finite-proof-finding–Emulate program for a limited number of steps; if it doesn’t do anything bad, assume it is safe19CS150 Fall 2005: Lecture 25: Undecidable ProblemsProof Recap•If we had is-virus? we could define halts?•We know halts? is undecidable•Hence, we can’t have is-virus?•Thus, we know is-virus? is undecidable20CS150 Fall 2005: Lecture 25: Undecidable ProblemsHow convincing is our Halting Problem proof? (define
View Full Document