This project aims to advance the technology for designing and implementing security-sensitive software for networked, embedded systems. The strategy unifies two approaches that can contribute key elements to the needed technology. The first approach provides security for distributed systems by using language-based information flow controls, a technique for annotating code with confidentiality and integrity requirements and using these requirements to determine the necessary placement of code in a networked system characterized by complex trust relations between distributed agents. The second approach, model-based design, expresses protocols and systems at a high level of abstraction suitable for automated analysis techniques that can reveal design errors, and provides synthesis tools that automate low-level platform-specific details, thereby reducing coding errors. The approach, called resource guided model transformation, will allow the designer to express systems and their security requirements at a high level, including annotations for resource constraints of the target platform. This research program focuses on the development of foundational theories and tools for correctness preserving transformations of these models and protocols, facilitating the synthesis of secure distributed software. The project investigates the effectiveness of this methodology by implementing secure transaction systems using Java Card technology.
