jha-security

I got a call from Byron Acohido over at the USA Today last weekend, and we had an interesting talk about botnets. Byron and Jon Swartz ended up writing an article about botnets which appeared as the cover story in the Money section of the USA Today on March 17, 2008. Here's a link to the full story ( link ). I found the entire article to be a fascinating read on the nature of botnets. Here are some of the highlights, but definitely go and read the entire article. On a typical day, 40% of the 800 million computers connected to the Internet are bots engaged in various nefarious activities, such as spamming, stealing sensitive data, and engaging in denial-of-service attacks. Think about it. Approximately 320 million computers are engaged these illicit actiivities! Later on in the article they describe various features of Storm , the state-of-the-art for botnets. Storm introduced various innovations into the bot landscape, such as using P2P style communication to converse with the bo...

Model checking is a technique of verifying temporal properties of finite-state systems. One of the attractive features of model checking over other techniques (such as theorem proving) is that if a property is not true, a model checker provides a counter-example which explains why the property is not true. Inventors of model checking, Edmund Clarke, Allen Emerson, and Joseph Sifakis, won the 2008 ACM Turing award (see the announcement here ). I have a personal connection to two of the recipients. Edmund Clarke was my adviser at Carnegie Mellon, and Allen Emerson and I have collaborated on few projects and he has supported me through out my career. In this note I try to summarize various applications of model checking to security. Protocol verification : Protocols in the realm of security (henceforth referred to as security protocols) are very tricky to get correct. For example, flaws in authentication protocols have been discovered several years after they have been published. Techniqu...