Declarative Infrastructure Configuration Synthesis and Debugging
Tóm tắt
There is a large conceptual gap between end-to-end infrastructure requirements and detailed component configuration implementing those requirements. Today, this gap is manually bridged so large numbers of configuration errors are made. Their adverse effects on infrastructure security, availability, and cost of ownership are well documented. This paper presents ConfigAssure to help automatically bridge the above gap. It proposes solutions to four fundamental problems: specification, configuration synthesis, configuration error diagnosis, and configuration error repair. Central to ConfigAssure is a Requirement Solver. It takes as input a configuration database containing variables, and a requirement as a first-order logic constraint in finite domains. The Solver tries to compute as output, values for variables that make the requirement true of the database when instantiated with these values. If unable to do so, it computes a proof of unsolvability. The Requirement Solver is used in different ways to solve the above problems. The Requirement Solver is implemented with Kodkod, a SAT-based model finder for first-order logic. While any requirement can be directly encoded in Kodkod, parts of it can often be solved much more efficiently by non model-finding methods using information available in the configuration database. Solving these parts and simplifying can yield a reduced constraint that truly requires the power of model-finding. To implement this plan, a quantifier-free form, QFF, is defined. A QFF is a Boolean combination of simple arithmetic constraints on integers. A requirement is specified by defining a partial evaluator that transforms it into an equivalent QFF. This QFF is efficiently solved by Kodkod. The partial evaluator is implemented in Prolog. ConfigAssure is shown to be natural and scalable in the context of a realistic, secure and fault-tolerant datacenter.
Tài liệu tham khảo
Security and Business Continuity Solutions from British Telecom: http://www.btglobalservices.com/business/global/en/products/docs/28154_219475secur_bro_single.pdf
Lampson, B: Computer security in real world. Annual Computer Security Applications Conference, 2000. http://research.microsoft.com/Lampson/64-SecurityInRealWorld/Acrobat.pdf
Oppenheimer, D., Ganapathy, A., Patterson, D.: Why do internet services fail and what can be done about it? 4th USENIX Symposium on Internet Technologies and Systems, 2003. http://roc.cs.berkeley.edu/papers/usits03.pdf
Schwartz, J.: Who Needs Hackers? New York Times, September 12, 2007. http://www.nytimes.com/2007/09/12/technology/techspecial/12threat.html
Kodkod: http://web.mit.edu/emina/www/kodkod.html
Torlak, E., Kodkod, D.J: A relational model finder. Tools and Algorithms for Construction and Analysis of Systems (TACAS ‘07). Braga, Portugal (March 2007). PDF, slides
ZChaff: http://www.princeton.edu/~chaff/
Mahajan, Y., Fu, Z., Malik, S.: Zchaff2004, an efficient SAT solver. Proceedings of 7th International Conference on Theory and Applications of Satisfiability Testing (SAT) (2004)
SWI-Prolog: http://www.swi-prolog.org/
Bratko, I.: Prolog Programming for Artificial Intelligence. Addison-Wesley International Computer Science Series (1990)
SWI-Prolog-JPL: http://www.swi-prolog.org/packages/jpl/prolog_api/overview.html
Narain, S.: Network configuration management via model-finding. Proceedings of USENIX Large Installation System Administration (LISA) Conference. San Diego, CA (2005)
Alloy: http://alloy.mit.edu/
Homer, J., Ou, X., McQueen, M.: From attack Graphs to Automated Configuration Management––an Iterative Approach Technical Report 2008-1, Computer Science Department, Kansas State University
Fu, Z., Malik S.: Solving the minimum-cost satisfiability problem using branch and bound search. Proceedings of IEEE/ACM International Conference on Computer-Aided Design ICCAD (2006)
Al-Shaer, E., Hamed, H.: Modeling and management of firewall policies. IEEE Transactions on Network and Service Management, vol. 1–1. (April, 2004)
Telcordia IPAssure: http://www.argreenhouse.com/papers/narain/TelcordiaIPAssure.pdf
Narain S., Cheng, T., Coan, B., Kaul V., Parmeswaran, K., Stephens, W.: Building autonomic systems via configuration. Proceedings of AMS Autonomic Computing Workshop, Seattle, WA (2003)
Barrett, C., Berezin, S.: CVC lite: A new implementation of the cooperating validity checker. In: Proceedings of the 16th International Conference on Computer Aided Verification (CAV ‘04). Lecture Notes in Computer Science, vol. 3114, pp. 515–518. Springer, Boston, Massachusetts (July, 2004)
Selman, B., Kautz, H.: Planning as satisfiability. Proceedings of ECAI-92. http://www.cs.cornell.edu/selman/papers/pdf/92.ecai.satplan.pdf