Quantitative information flow (QIF) is a new notion based on information theory for expressing how much a program leaks information to an external observer. We aim to develop a method for modifying a given program so that QIF of the program does not exceed a given threshold value as a security requirement. In this study, we examine an approach to inserting "filters" to reduce QIF. A Filter restricts the input or output domain of a program, and forces a program to abort if the input or output is out of the restricted domain.
In this thesis, we first show that the problem of finding the optimal filter that maximizes the input domain while satisfying a given security requirement is PP-hard. Thus, the optimization problem is computationally hard in general. Also it has been known that even computing QIF of a loop-free program is #P-complete. For these reasons, we find a property called (N,e)-monotonicity of a program and a filter such that if the property holds, we can easily estimate a reasonable upper bound of QIF of the program with the filter using SAT-based QIF analysis technique. Lastly, the thesis shows the experimental results conducted on a few programs in C language by using existing tools CBMC and sharp CDCL.