Type-Driven Repair for Information Flow Security

摘要: We present Lifty, a language that uses type-driven program repair to enforce information flow policies. In the programmer specifies policy by annotating source of sensitive data with refinement type, and system automatically inserts access checks necessary this across code. This is significant improvement over current practice, where programmers manually implement checks, any missing check can cause an leak. To support programming model, we have developed (1) encoding security in terms decidable types enables fully automatic verification (2) algorithm localizes unsafe accesses replaces them provably secure alternatives. formalize prove its noninterference guarantee. Our experience using Lifty conference management shows it decreases burden able efficiently synthesize all including those required prevent set reported real-world leaks.