Jeddak: Abstractions for Secure Distributed Applications

Summary: Develop abstractions for secure distributed application development, based on relating the use of cryptographic libraries to the end-to-end security guarantees that those operations are intended to achieve.

Personnel: Tom Chothia, Dominic Duggan, Jan Vitek (Purdue University), Ye Wu.

Funding: National Science Foundation, WinSeC.

Web: Jeddak Project.

Access Control and Downgrading in Information Flow Assurance

Summary: Develop policy language to specify confidentiality and integrity goals including expressive downgrading policies. Develop automated enforcement tools based on static analysis of code. Representative papers appear in the 27th, 28th and 29th IEEE Symposia on Security and Privacy.

Personnel: David Naumann, Anindya Banerjee (Kansas State Univ and IMDEA Madrid), Stan Rosenberg, and external collaborators at IBM Research, Microsoft Research, INRIA France, and Chalmers University of Technology.

Funding: National Science Foundation.

Web: SecJ System

A JML Community Infrastructure

Summary: Formal specification and analysis tools for Java software, based on unified machine-checked semantic model. Representative paper at the 22d ACM Symposium on Object-Oriented Programming, Systems, Languages, and Applications.

Personnel: David Naumann, Stan Rosenberg, Gary Leavens (U. Central Florida), Curt Clifton (Rose-Hullman), Yoonsik Cheon (U. Texas, El Paso), Hridesh Rajan (Iowa State), Robby (Kansas State), Samik Basu (Iowa State)

Funding: National Science Foundation.

Web: Java Modeling Language

Specification Language Foundations for Modular Reasoning Methodologies

Summary: This project will provide guidance for the designers of programming and specification languages, verification logics, and associated tools. It will allow the future development of highly trustworthy methodologies. The results will improve the utility and extensibility of verification tools and runtime assertion checkers. Software developers will benefit from the integration and harmonious interoperation of best-practice methodologies.

Personnel: David Naumann, Stan Rosenberg, Gary Leavens (U. Central Florida)

Funding: National Science Foundation.

Security and High Assurance for Wireless Networking

Summary: Model and analyse wireless network protocols and applications, to find vulnerabilities and develop infrastructure for usable and secure interoperation between technologies.

Personnel:Susanne Wetzel, David Naumann, Alex Myasnikov, Chunyu Tang

Funding:US Government, Telcordia Technologies, NJ Commission on Science and Technology

Privacy-Preserving Publishing Data with Outliers

Summary: Study the problem of anonymizing microdata that contains outliers. Representative paper at the 12th International Conference on Extending Database Technology (EDBT)

Personnel: Wendy Hui Wang, Ruilin Liu

Privacy-Preserving Publishing Trajectory Databases

Summary: Study the problem of anonymizing the trajectory databases. Representative paper at the 12th International Conference on Extending Database Technology (EDBT)

Personnel: Wendy Hui Wang, Roman Yarovoy (University of British Columbia), Francesco Bonchi (Yahoo! Research), Laks V. S. Lakshmanan (University of British Columbia)

Privacy-Preserving Data Publishing with Low Information Loss

Summary: Study the problem of anonymizing the microdata with low information loss. Representative paper at the the 14th International Conference on Management of Data (COMAD).

Personnel: Wendy Hui Wang

Mobile Access Control

Summary: Extend role-based access control to encompass mobility and location-based services.

Personnel: Adriana Compagnoni, Elsa Gunter (U. Illinois), Pablo Garralda

Funding: National Science Foundation, WiNSeC

Web: Mobile access control

A Formally Verified Environment For The Production Of Secure Software

Summary: This project studies new architectures for verifiably safe execution of software.

Personnel: David Aspinall, Adriana Compagnoni, Ricardo Medel, Eduardo Bonelli, and Matthieu Lucotte.

Funding:National Science Foundation CAREER, NSF ITR, NJ Commission on Science and Technology

Web: Heap Bounded Assembly Language and also Information Flow Analysis for Assembly Languages

Malware Analysis and Botnet Tracking

Summary: This project studies new forms of malware and their network behavior.

Personnel: Sven Dietrich