We present a novel formal system for proving quantitative-leakage properties of programs. Based on a theory of Quantitative Information Flow (QIF) that models information leakage as a noisy communication channel, it uses "gain-functions" for the description and measurement of expected leaks. We use a small imperative programming language, augmented with leakage features, and with it express adversaries' activities in the style of, but more generally than, the Hoare triples or expectation transformers that traditionally express deterministic or probabilistic correctness but without information flow. The programs are annotated with "gain-expressions" that capture simple adversarial settings such as "Guess the secret in one try." but also much more general ones; and our formal syntax and logic -based framework enables us to transform such gain-expressions that apply after a program has finished to ones that equivalently apply before the program has begun. In that way we enable a formal proof-based reasoning system for QIF at the source level. We apply it to the %programming language we have chosen, and demonstrate its effectiveness in a number of small but sometimes intricate situations.

翻译：我们提出了一种新颖的形式化系统，用于证明程序的定量泄漏特性。该系统基于将信息泄漏建模为噪声通信信道的定量信息流理论，采用"增益函数"来描述和测量预期泄漏。我们使用一种增加了泄漏特性的小型命令式编程语言，并以此表达对手活动——其风格类似于但不限于传统上用于表达确定性或概率正确性（但不涉及信息流）的Hoare三元组或期望转换器。程序通过"增益表达式"进行标注，这些表达式既能捕捉简单的对抗场景（如"一次猜中秘密"），也能描述更一般的情况；我们基于形式语法和逻辑的框架使得能够将程序结束后适用的增益表达式，转换为在程序开始前等效适用的表达式。通过这种方式，我们实现了在源码层面进行基于形式化证明的定量信息流推理系统。我们将该系统应用于所选编程语言，并通过多个小型但有时复杂的场景验证了其有效性。