|
|||||
|
My primary research at Penn has been in network security. In particular, I have worked on formalizing the concept of secure tunnels in the design of the Tunnel Calculus. The calculus has primarily been applied to protocols discover and negotiate security gateways. I have also did some work in the area of embedded systems. Many years ago I performed research in computer algebra as part of my masters studies in mathematics. My papers are listed below. Network Security - Secure Tunnels Secure tunnels provide a secure communication link over an insecure Internet. They are particularly valuable for secure electronic commerce transactions, such as online transactions over TLS, and for remote access to enterprise networks such as VPNs based on IPsec. They have proved more problematic in other contexts such as the use of WEP to provide link-layer tunnels across 802.11(b) wireless networks. A major question in this area is how to relate different tunneling services to ensure the desired global behavior. For instance, a typical user may build a link-layer tunnel to a wireless access point, layer on top of this a network-layer tunnel to an enterprise network, and then use an SSL tunnel to complete a link to a secure web site. More complicated combinations may arise when operations such as accounting are involved (to pay for cellular data access for instance). Architectures and protocols to organize groups of tunnels are not yet well-developed and largely have not been deployed. In many cases today, different tunneling technologies (WEP, TLS, etc.) are used in a single protocol. We believe thatthis has been an impediment to the design of protocols to up complex of tunnels. Our investigations have shown that it is possible to restrict ourselves to the use network layer (layer 3) tunneling mechanisms, namely IPsec, for the protocols of interest. Our first foray into designing protocols that set up a collection of tunnels was targeted at the application of protecting the wireless accounting infrastructure. This seemingly simple protocol turned out to be quite difficult to get right. As a result it was subjected to relatively extensive formal analysis as well as a prototype implementation. My current focus is on protocols for discovery negotiation of security gateways. Getting these protocols correct is are even more fraught with peril than the L3A protocol. This has inspired me to design a formalism, the tunnel calculus, to formulate and reason about such protocols. We hope to apply the calculus to other types of discovery protocols. A more detailed description of my work in this area can be found on the Tunnel Calculus page. Open Embedded Systems (OpEm) Most embedded systems are programmed at the factory. Unlike PCs, a user can not get a program written by a third party to control his fridge, vacuum cleaner, or car. We believe that this will change and that users will want the kind of flexibility that they have come to expect in other computing devices. For the past several years the OpEm project here at Penn has been researching technologies and methods that enable third parties to program embedded systems. The first platform used in our investigations was microwave ovens. Current microwave ovens already have some degree of programmability. Newer ovens have multiple heating sources and several sensors that combine to produce better food. Unfortunately they are more difficult to program than most current models. We had the idea of delivering a program on the box with pre-packaged food. The program will be delivered in the form of a two-dimensional bar code. We also used model checking tools to verify that the programs don't cause any harm. A paper describing this work can be found below. The OpEm project has moved on from microwave ovens and now concentrates on smart cards. Using the Global Platform and JavaCard architectures, we have designed a mechanism that allows third parties to place their own policies on a Java Card. For example, if a credit card company used our technology, then you could obtain one for your child to use while away at school and program it to restrict what your child bought, where they bought it from, and how much they spent. This work has received a lot of press. For related work see Michael McDougall's dissertation. Computer Algebra About a decade ago I did a masters degree in mathematics. My thesis was in Computer Algebra. In particular, I developed algorithms and data structures for computing over graded rings. Papers
|
|
||||