[Logic and Complexity] Fwd: Talk: Dr. Limin Jia From CMU Cylab

[Yijia Chen]

 -------- Original Message --------
 Subject: Talk: Dr. Limin Jia From CMU Cylab
 Date: Mon, 22 Apr 2013 08:29:32 +0800
 From: Kenny Zhu <kzhu at cs.sjtu.edu.cn>
 To: all at cs.sjtu.edu.cn
 Cc: Limin Jia <liminjia at cmu.edu>


 Dear all,

 It's my pleasure to welcome Dr. Limin Jia from CMU to visit us and give
 a talk on secure programming on Android. Dr Jia will stay after the 
 talk
 to interact with students and faculty who might be interested in her
 research. Please disseminate this information to your students.

 Thanks,

 Kenny

 *************************************************************************************Talk
 Title: Run-Time Enforcement of Information-Flow Properties on Android
 Time: Tuesday, April 23, 2 PM
 Venue: Room 3-414

 Abstract:
 I will talk about improving Android's permission system to prevent
 confused-deputy attacks and information leakage. Our system permits
 Android applications to be concisely annotated with information-flow
 policies by either the programmers or security analysts. We develop a
 detailed model of our enforcement system using a process calculus, and
 use the model to prove noninterference. Our system and model have a
 number of useful or novel features, including support for Android's
 single- and multiple-instance components, floating labels,
 declassification and endorsement capabilities, and support for legacy
 applications. Our system design fits the Android programming model
 and runtime cleanly enough that we have developed a fully functional
 prototype on Android 4.0.4. We have tested our prototype on a Nexus S
 phone, verifying that it can enforce practically useful policies that
 can be implemented with minimal modification to off-the-shelf
 applications.

 Bio: Limin Jia is a Research Systems Scientist at CyLab at Carnegie
 Mellon University. She received her Ph.D. in Computer Science from
 Princeton University. Her research interests include programming
 languages, language-based security, logic, and program
 verification. At CyLab, Limin's research focuses on formal aspects of
 security. She is particularly interested in applying language-based
 security techniques as well as formal logic to model and verify
 security properties of software systems.