On Sat, Apr 12, 2008 at 12:34 AM, Matt Mahoney <[EMAIL PROTECTED]> wrote: > > Actually it cannot be solved even theoretically. A formal specification of a > program is itself a program. It is undecidable whether two programs are > equivalent. (It is equivalent to the halting problem). > > Converting natural language to a formal specification is AI-hard, or perhaps > harder, because people can't get it right either. If we could write software > without bugs, we would solve a big part of the security problem. >
You just evoked a Halting Problem Fallacy. You can't check if given arbitrary program terminates, but you can write a program that provably terminates. Likewise you can't check correctness of an arbitrary program, but you can write a provably correct program. Yes, it is possible to write software without bugs, starting from a formal definition of what 'bug' is (for example, 'it must never crash', 'it must never directly leak sensitive data' or 'it must continue to be able perform function A properly' are OK). The cause for this whole security problem thing is that presently it's very hard to write provably safe programs, so almost no one is doing it. Functional programming research community is working on this problem, but I doubt there will ever be tools that will enable average Joe the programmer to meaningfully write verified code. Understanding natural language specification and converting it to code is what programming is about. I certainly didn't imply that 'programming is unnecessary, perfect secure code can just write itself'. It won't happen until we have AGI. > > > These AIs for network security that you are talking about are a > > cost-effective hack that happens to work sometimes. It's not a > > low-budget vision of future super-hacks. > > Not at present because we don't have AI. I responded assuming that you were talking about the following sort of thing, and its presumed further development to higher levels and subtler rules: http://en.wikipedia.org/wiki/Intrusion-prevention_system "Rate based IPS (RBIPS) are primarily intended to prevent Denial of Service and Distributed Denial of Service attacks. They work by monitoring and learning normal network behaviors. Through real-time traffic monitoring and comparison with stored statistics, RBIPS can identify abnormal rates for certain types of traffic e.g. TCP, UDP or ARP packets, connections per second, packets per connection, packets to specific ports etc. Attacks are detected when thresholds are exceeded. The thresholds are dynamically adjusted based on time of day, day of the week etc., drawing on stored traffic statistics." > We rely on humans to find > vulnerabilities in software. We would like for machines to do this > automatically. Unfortunately such machines would also be useful to hackers. > Such double-edged tools already exist. For example, tools like SATAN, > NESSES, > and NMAP can quickly test a system by probing it to look for thousands of > known or published vulnerabilities. Attackers use the same tools to break > into systems. www.virustotal.com allows you to upload a file and scan it > with > 32 different virus detectors. This is a useful tool for virus writers who > want to make sure their programs evade detection. I suggest it will be very > difficult to develop any security tool that you could keep out of the hands > of > the bad guys. > All automatic tools already work from formally specified things that they are trying to find in the system. If you write the code so that these things are not there, and ascertain it by using automatic verification based on e.g. sufficiently rich type system, these tools won't find anything either. And yes, if you don't make code clearer, it's a very difficult problem to find vulnerabilities in it, and the smarter/more resourceful you are, the more you'll be able to find. -- Vladimir Nesov [EMAIL PROTECTED] ------------------------------------------- singularity Archives: http://www.listbox.com/member/archive/11983/=now RSS Feed: http://www.listbox.com/member/archive/rss/11983/ Modify Your Subscription: http://www.listbox.com/member/?member_id=4007604&id_secret=98631122-712fa4 Powered by Listbox: http://www.listbox.com
