%0 Conference Proceedings %T Uniform Protection for Multi-exposed Targets %+ Danmarks Tekniske Universitet = Technical University of Denmark (DTU) %A Vigo, Roberto %A Nielson, Flemming %A Nielson, Hanne, Riis %Z Part 3: Security Analysis %< avec comité de lecture %( Lecture Notes in Computer Science %B 34th Formal Techniques for Networked and Distributed Systems (FORTE) %C Berlin, Germany %Y Erika Ábrahám %Y Catuscia Palamidessi %I Springer %3 Formal Techniques for Distributed Objects, Components, and Systems %V LNCS-8461 %P 182-198 %8 2014-06-03 %D 2014 %R 10.1007/978-3-662-43613-4_12 %K Security verification %K distributed systems %K protection analysis %K security cost %K Quality Calculus %K Satisfiability Modulo Theories %Z Computer Science [cs] %Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers %X Ensuring that information is protected proportionately to its value is a major challenge in the development of robust distributed systems, where code complexity and technological constraints might allow reaching a key functionality along various paths. We propose a protection analysis over the Quality Calculus that computes the combinations of data required to reach a program point and relates them to a notion of cost. In this way, we can compare the security deployed on different paths that expose the same resource. The analysis is formalised in terms of flow logic, and is implemented as an optimisation problem encoded into Satisfiability Modulo Theories, allowing us to deal with complex cost structures. The usefulness of the approach is demonstrated on the study of password recovery systems. %G English %Z TC 6 %Z WG 6.1 %2 https://inria.hal.science/hal-01398016/document %2 https://inria.hal.science/hal-01398016/file/978-3-662-43613-4_12_Chapter.pdf %L hal-01398016 %U https://inria.hal.science/hal-01398016 %~ IFIP-LNCS %~ IFIP %~ IFIP-TC %~ IFIP-WG %~ IFIP-TC6 %~ IFIP-WG6-1 %~ IFIP-FORTE %~ IFIP-LNCS-8461