Local mirror of The Unified Policy Framework (UPF) entry of the Archive of Formal Proofs (AFP). https://www.isa-afp.org/entries/UPF_Firewall.shtml
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 

87 lines
4.6 KiB

  1. To cite the use of this formal theory, please use
  2. Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Formal Network
  3. Models and Their Application to Firewall Policies. In Archive of Formal
  4. Proofs, 2017. http://www.isa-afp.org/entries/UPF_Firewall.shtml,
  5. Formal proof development.
  6. A BibTeX entry for LaTeX users is
  7. @Article{ brucker.ea:upf-firewall:2017,
  8. abstract = {We present a formal model of network protocols and their application to modeling firewall policies. The formalization is based on the \emph{Unified Policy Framework} (UPF). The formalization was originally developed with for generating test cases for testing the security configuration actual firewall and router (middle-boxes) using HOL-TestGen. Our work focuses on modeling application level protocols on top of tcp/ip.},
  9. author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
  10. date = {2017-01-08},
  11. file = {https://www.brucker.ch/bibliography/download/2017/brucker.ea-upf-firewall-outline-2017.pdf},
  12. filelabel = {Outline},
  13. issn = {2150-914x},
  14. journal = {Archive of Formal Proofs},
  15. month = {jan},
  16. note = {\url{http://www.isa-afp.org/entries/UPF_Firewall.shtml}, Formal proof development},
  17. pdf = {https://www.brucker.ch/bibliography/download/2017/brucker.ea-upf-firewall-2017.pdf},
  18. title = {Formal Network Models and Their Application to Firewall Policies},
  19. url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-upf-firewall-2017},
  20. year = {2017},
  21. }
  22. An overview of the formalization is given in:
  23. Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Formal Firewall
  24. Conformance Testing: An Application of Test and Proof Techniques. In
  25. Software Testing, Verification & Reliability (STVR), 25 (1), pages
  26. 34-71, 2015.
  27. https://www.brucker.ch/bibliography/abstract/brucker.ea-formal-fw-testing-2014
  28. A BibTeX entry for LaTeX users is
  29. @Article{ brucker.ea:formal-fw-testing:2014,
  30. abstract = {Firewalls are an important means to secure
  31. critical ICT infrastructures. As configurable
  32. off-the-shelf prod\-ucts, the effectiveness of a
  33. firewall crucially depends on both the correctness
  34. of the implementation itself as well as the
  35. correct configuration. While testing the
  36. implementation can be done once by the
  37. manufacturer, the configuration needs to be tested
  38. for each application individually. This is
  39. particularly challenging as the configuration,
  40. implementing a firewall policy, is inherently
  41. complex, hard to understand, administrated by
  42. different stakeholders and thus difficult to
  43. validate. This paper presents a formal model of
  44. both stateless and stateful firewalls (packet
  45. filters), including NAT, to which a
  46. specification-based conformance test case
  47. gen\-eration approach is applied. Furthermore, a
  48. verified optimisation technique for this approach
  49. is presented: starting from a formal model for
  50. stateless firewalls, a collection of
  51. semantics-preserving policy transformation rules
  52. and an algorithm that optimizes the specification
  53. with respect of the number of test cases required
  54. for path coverage of the model are derived. We
  55. extend an existing approach that integrates
  56. verification and testing, that is, tests and
  57. proofs to support conformance testing of network
  58. policies. The presented approach is supported by a
  59. test framework that allows to test actual
  60. firewalls using the test cases generated on the
  61. basis of the formal model. Finally, a report on
  62. several larger case studies is presented.},
  63. author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
  64. doi = {10.1002/stvr.1544},
  65. journal = {Software Testing, Verification & Reliability (STVR)},
  66. keywords= {model-based testing; conformance testing; security
  67. testing; firewall; specification-based testing;
  68. testing cloud infrastructure, transformation for
  69. testability; HOL-TestGen; test and proof; security
  70. configuration testing},
  71. language= {USenglish},
  72. number = {1},
  73. pages = {34--71},
  74. pdf = {https://www.brucker.ch/bibliography/download/2014/brucker.ea-formal-fw-testing-2014.pdf},
  75. publisher= {John Wiley & Sons},
  76. title = {Formal Firewall Conformance Testing: An Application of Test and Proof Techniques},
  77. url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-formal-fw-testing-2014},
  78. volume = {25},
  79. year = {2015},
  80. }