338H IST Building
University Park, PA 16802
Phone: (1) 814-863-7323
E-mail: zhang (domain: cse.psu.edu)
Danfeng Zhang is an Assistant Professor at Penn State University. He
received his B.S. and M.S. in Computer Science from Peking University, and his
Ph.D. in Computer Science from Cornell University.
His research focuses on computer security and programming languages. His recent
work is on sound and practical methods for full-system mitigation of timing
channels and a general approach of diagnosing errors detected by static program
analyses, such as information-flow analyses and ML type inference.
I'm looking for highly-motivated and outstanding PhD applicants who are
interested in security and programming languages. Research opportunities are
also available for Penn State undergraduates. Please send me an email if
Full-system timing channel mitigation: Timing
channels are long-standing threats to information security. Since computation
time is affected by both software and hardware, detecting and preventing timing
channels at a single level is doomed to fail. To fully address this threat, an
integrated approach to system security is proposed, in which security is
enforced at the software level, at the hardware level, and across the
General methods of errors localization: Localizing program errors (both
static errors and dynamic errors) is still an extremely time consuming task.
For example, sophisticated program analyses, such as ML type inference and
information flow analyses, tend to generate confusing error messages when the
analyses fail. We look for general and precise methods for localizing program
errors. The insight is that the likelihood of different error explanations can
effectively be evaluated on the structure of a graph describing system behavior.
Language-based differential privacy proofs: The growing popularity of
differential privacy has resulted in the development of increasingly
sophisticated differentially private algorithms, accompanied by a corresponding
increase in the development of incorrect algorithms with flawed proofs of
privacy. We explore light-weight type systems to simplify and automate most
parts of the proofs for sophisticated algorithms.