A Domain-Specific Language for Filtering in Application-Level Gateways
Balldin, Hampus and Reichenbach, Christoph LU
(2020)
19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2020
p.111-123
- Abstract
- Application-level packet filtering is a technique for network access control in which an “application-level gateway” intercepts network packets at the application level (e.g., HTTP, FTP), scans them for security concerns and optionally logs, rewrites or discards them. Existing application-level filters express their filtering rules in general-purpose languages, which limits the correctness guarantees available for them. We present the first declarative language for application-level network filtering, developed at Advenica AB. Our DSL uses security assertions to express properties that packets must have to be allowed through the network (e.g., “IMAP packet contains no executable attachment” or “SQL reply contains only explicitly permitted... (More)
- Application-level packet filtering is a technique for network access control in which an “application-level gateway” intercepts network packets at the application level (e.g., HTTP, FTP), scans them for security concerns and optionally logs, rewrites or discards them. Existing application-level filters express their filtering rules in general-purpose languages, which limits the correctness guarantees available for them. We present the first declarative language for application-level network filtering, developed at Advenica AB. Our DSL uses security assertions to express properties that packets must have to be allowed through the network (e.g., “IMAP packet contains no executable attachment” or “SQL reply contains only explicitly permitted columns”), along with remedies that either reject or rewrite undesirable packets. We have designed the language around the needs of network filter developers, with a focus on correctness: our language can statically verify several properties of filter programs, such as well-formedness of the outcome, confluence, and termination, with the help of an off-the-shelf SMT solver. Our initial results show that the language can express many typical filtering tasks, closely maps to the application domain, and provides strong correctness guarantees. (Less)
Please use this url to cite or link to this publication:
https://lup.lub.lu.se/record/da622418-caad-4610-bc0a-ff8eb2bd0346
- author
- Balldin, Hampus
and Reichenbach, Christoph
LU
- organization
- publishing date
- 2020-11
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- network security, domain-specific languages, packet filtering, filtering language
- host publication
- Proceedings of the 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences
- pages
- 111 - 123
- publisher
- Association for Computing Machinery (ACM)
- conference name
- 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2020
- conference location
- Virtual, United States
- conference dates
- 2020-11-16 - 2020-11-17
- external identifiers
-
- scopus:85097655222
- ISBN
- 9781450381741
- DOI
- 10.1145/3425898.3426955
- project
- WASP startup package Christoph Reichenbach
- language
- English
- LU publication?
- yes
- id
- da622418-caad-4610-bc0a-ff8eb2bd0346
- date added to LUP
- 2020-11-17 20:38:45
- date last changed
- 2022-04-19 02:08:51
@inproceedings{da622418-caad-4610-bc0a-ff8eb2bd0346,
abstract = {{Application-level packet filtering is a technique for network access control in which an “application-level gateway” intercepts network packets at the application level (e.g., HTTP, FTP), scans them for security concerns and optionally logs, rewrites or discards them. Existing application-level filters express their filtering rules in general-purpose languages, which limits the correctness guarantees available for them. We present the first declarative language for application-level network filtering, developed at Advenica AB. Our DSL uses security assertions to express properties that packets must have to be allowed through the network (e.g., “IMAP packet contains no executable attachment” or “SQL reply contains only explicitly permitted columns”), along with remedies that either reject or rewrite undesirable packets. We have designed the language around the needs of network filter developers, with a focus on correctness: our language can statically verify several properties of filter programs, such as well-formedness of the outcome, confluence, and termination, with the help of an off-the-shelf SMT solver. Our initial results show that the language can express many typical filtering tasks, closely maps to the application domain, and provides strong correctness guarantees.}},
author = {{Balldin, Hampus and Reichenbach, Christoph}},
booktitle = {{Proceedings of the 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences}},
isbn = {{9781450381741}},
keywords = {{network security; domain-specific languages; packet filtering; filtering language}},
language = {{eng}},
pages = {{111--123}},
publisher = {{Association for Computing Machinery (ACM)}},
title = {{A Domain-Specific Language for Filtering in Application-Level Gateways}},
url = {{https://lup.lub.lu.se/search/files/86952957/gpce2020.pdf}},
doi = {{10.1145/3425898.3426955}},
year = {{2020}},
}