SKLCS Seminar 

　　Title: Averting Distributed Covert Channels Through Mathematics-Based Design 

　　Speaker: Ridha Khedri (McMaster University, Cananda) 

　　          www.cas.mcmaster.ca/~khedri 

　　Time: 27th May 2015, 09:50 

　　Venue: Seminar Room (334), Level 3, Building 5, Institute of Software, CAS 

　　Abstract:   

　　Software systems contain paths for information transmission that were not intended by their designers. These paths utilize the systems' resources, environment, or established legitimate communication channels. They are called distributed covert channels and can be used as paths to leak out confidential information to unauthorized recipients. To the unwary user, these channels may transport information as if by magic, despite the vigilance of monitors. Because of this, covert channels pose a significant threat to information security. In a system of communicating agents, if there exists a covert channel, then two conditions are satisfied: Constraint on Communication and Potential for Communication. 

　　In this talk, we present Communicating Concurrent Kleene Algebra (C2KA), which is an extension of Hoare's latest theory that unifies diverse theories for conventional sequential and parallel programs.  Then, we use it to model and reason on distributed covert channels.  We focus our discussion on only the potential for communication condition. At the end, we show how the obtained mathematical results help us design systems that are resilient to covert channels.