UVA CS 150 - Proving Uncomputabili ty

Unformatted text preview:

Slide 1From Paul Graham’s “Undergraduation”:Morris Internet Worm (1988)Worm Detection ProblemUncomputability ProofSlide 6“Solving” Undecidable ProblemsConclusion?Actual is-virus? ProgramsProof RecapHow convincing is our Halting Problem proof?History of Object-Oriented ProgrammingPre-History: MIT’s Project Whirlwind (1947-1960s)Why Whirlwind?Whirlwind InnovationsSketchpadComponents in SketchpadObjects in SketchpadSimulaCounter in SimulaXEROX Palo Alto Research Center (PARC)Dynabook, 1972Dynabook 1972BYTE Magazine, August 1981SmalltalkCounter in SmalltalkCounter Object in SchemeCounter in PythonWho was the first object-oriented programmer?Slide 30David Evanshttp://www.cs.virginia.edu/evansCS150: Computer ScienceUniversity of VirginiaComputer ScienceLecture 26: Lecture 26: Proving Proving UncomputabiliUncomputabilityty2Lecture 26: Proving ComputabilityFrom 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+ fine3Lecture 26: Proving ComputabilityMorris 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)4Lecture 26: Proving ComputabilityWorm 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 specification POutput: true if evaluating (P) would cause a file on the host computer to be “infected”.5Lecture 26: Proving ComputabilityUncomputability ProofSuppose we could define is-virus? Then:(define (halts? P) (is-virus? ‘(lambda () (begin ((remove-infects P)) (infect-files)))))6Lecture 26: Proving ComputabilityUncomputability Proof(define (halts? P) (is-virus? ‘(lambda () (begin ((remove-infects P)) (infect-files)))))#t: Since it is a virus, we know (infect-files) was evaluated, and P must halt.#f: The (infect-files) would not evaluate, so P must not halt.Can we make remove-infects?Yes, just removeall file writes.7Lecture 26: Proving Computability“Solving” Undecidable Problems•No perfect solution exists:–Undecidable means there is no procedure that:•Always gives the correct answer•Always terminates•Must give up one of these to “solve” undecidable problems–Giving up #2 is not acceptable in most cases–Must give up #1•Or change the problem: e.g., detect file infections during an execution8Lecture 26: Proving ComputabilityConclusion?•Anti-Virus programs cannot exist!“The Art of Computer Virus Research and Defense”Peter Szor, Symantec9Lecture 26: Proving ComputabilityActual 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 safe10Lecture 26: Proving ComputabilityProof 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 undecidable11Lecture 26: Proving ComputabilityHow convincing is our Halting Problem 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!This “proof” assumes Scheme exists and is consistent!12Lecture 26: Proving ComputabilityHistory ofObject-Oriented Programming13Lecture 26: Proving ComputabilityPre-History:MIT’s Project Whirlwind (1947-1960s)Jay Forrester14Lecture 26: Proving ComputabilityWhy Whirlwind?Hiroshima (12kt), Nagasaki (20kt)First H-Bomb (10Mt)Tsar Bomba (largest ever)B83 (1.2Mt), largestin currently active arsenalfrom Class 2...Soviet Union test atomic bomb (Aug 29, 1949)15Lecture 26: Proving ComputabilityWhirlwind InnovationsMagnetic Core Memory(first version used vacuum tubes)16Lecture 26: Proving ComputabilitySketchpad•Ivan Sutherland, 1963 (PhD thesis supervised by Claude Shannon)•Interactive drawing program•Light penhttp://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-574.pdf17Lecture 26: Proving ComputabilityComponents in Sketchpad18Lecture 26: Proving ComputabilityObjects in SketchpadIn the process of making the Sketchpad system operate, a few very general functions were developed which make no reference at all to the specific types of entities on which they operate. These general functions give the Sketchpad system the ability to operate on a wide range of problems. The motivation for making the functions as general as possible came from the desire to get as much result as possible from the programming effort involved. For example, the general function for expanding instances makes it possible for Sketchpad to handle any fixed geometry subpicture. The rewards that come from implementing general functions are so great that the author has become reluctant to write any programs for specific jobs. Each of the general functions implemented in the Sketchpad system abstracts, in some sense, some common property of pictures independent of the specific subject matter of the pictures themselves. Ivan Sutherland, Sketchpad: a Man-Machine Graphical Communication System, 1963 (major influence on Alan Kay


View Full Document

UVA CS 150 - Proving Uncomputabili ty

Documents in this Course
Objects

Objects

6 pages

Load more
Download Proving Uncomputabili ty
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Proving Uncomputabili ty and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Proving Uncomputabili ty 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?