SoS Quarterly Summary Report - Apr to Jun 2014
Lablet Summary Report
Purpose: To highlight progress. Information is generally at a higher level which is accessible to the interested public.
A). Fundamental Research
[Xie, Blythe, Koppel, Smith] Continued exploration of DASH models with an eye towards choosing scenarios to model in a multi-agent setting, the hypotheses to initially explore, and how to validate the resulting models. Developing tool support to extract contextual information of using permissions for a mobile app so that users of the mobile app can view more detailed information for determining whether the mobile app may be a malicious app or not. Exploring using NLP/automatic text analysis on problem reports and change logs from partner IT departments, and also using these techniques on the open-ended responses to our questionnaire.
[Godfrey, Caesar, Nicol, Sanders, Jin] Developed an initial design to model network behavior under timing uncertainty. Began to design new network models and algorithms for testing hypothesis related to general network wide properties, such as reachability, end-to-end delay and throughput, and conducted preliminary experiments using VeriFlow, a system developed under our earlier SoS lablet, to inform our designs.
[Iyer, Kalbarczyk] Focused on a novel application of Factor Graphs to represent real-world security incidents and develop a scientifically sound method for preemptive detection of attacks, i.e., before the system misuse.
[Mitra, Dullerud, Chaudhuri] Developed a technique for deciding bounded time safety properties of deterministic nonlinear hybrid models. These models can capture a wide range of cyberphysical systems. Formulated a computational problem in automated synthesis of alternating periodic controllers with a model of an adversary that adds arbitrary controls inputs. We are currently experimenting with solving these alternating games using SMT solvers.
[Sanders, Bashir, Nicol, Van Moorsel] Goal to develop quantitative, scientifically grounded, decision-making tools to guide information security investments in private or public organizations, combining human and technological concerns, to demonstrate their use in two or more real-life case studies, and validate the usefulness of the tools through analysis of the results of the completed case studies.
We're seeing really good foundational work in modeling human behavior with respect to the way that humans can try to circumvent security measures. The importance of this is that models like these help us to understand what humans try to get around, why they try to get around it, and thus how to security controls that are equally protective, yet more useable..
B). Community Interaction
[Sanders, Bashir, Nicol, Van Moorsel] July 2014 SoS PI Quarterly meeting talk by Bill Sanders which has been uploaded to the CPS-VO.
[Xie, Blythe, Koppel, Smith] Blythe presented paper at ACySE in May. Smith and Koppel JAMIA paper on usability problems with health IT was named "among most significant papers of the year."
[Godfrey, Caesar, Nicol, Sanders, Jin] Jin and Ning, "Securing Industrial Control Systems with a Simulation-based Verification System," In Proceedings of the 2014 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation, Denver, CO, May 2014.
[Iyer, Kalbarczyk] Presented two posters at Symposium and Bootcamp on the Science of Security (HotSoS), April 2014, Raleigh, NC. Paper submission to Workshop on Learning from Authoritative Security Experiment Results (LASER) 2014, "An Experiment Using Factor Graph for Early Attack Detection."
[Mitra, Dullerud, Chaudhuri] Organized a kickoff meeting in February during which Prof. Chaudhuri visited Illinois and different adversary models, and relevant analysis techniques were discussed in a day long technical meeting. Mitra presented at Symposium and Bootcamp on the Science of Security (HotSoS), April 2014, Raleigh, NC (Proving Abstractions of Dynamical Systems through Numerical Simulations). In Computer Aided Verification (CAV2014), Vienna, Austria (Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells).
C. Educational
Two summer internships were provided this summer. One to a University of Illinois student and one to a Tennessee State University student. The interns worked on developing tools and methodologies for proving connectivity properties of networks across several layers of the network stack.