Esta Tese aplica métodos formais, e em particular o framework de Fluxo de Informação Quantitativo (QIF), para criar modelos escaláveis para grandes conjuntos de dados e pipelines de software que processam dados. Ao dividir sistemas complexos em seus componentes, pode-se explicar rigorosamente as vulnerabilidades de privacidade e como combatê-las afetaria a utilidade dos dados.