TY - GEN
T1 - DISV
T2 - 44th IEEE Symposium on Security and Privacy Workshops, SPW 2023
AU - Kumar, Ashish
AU - Harris, Bill
AU - Tan, Gang
N1 - Publisher Copyright:
© 2023 IEEE.
PY - 2023
Y1 - 2023
N2 - Data format specification languages such as PDF or HTML have been used extensively for exchanging structured data over the internet. While receivers of data files (e.g., PDF viewers or web browsers) perform syntax validation of files, validating deep semantic properties has not been systematically explored in practice. However, data files that violate semantic properties may cause unintended effects on receivers, such as causing them to crash or creating security breaches, as recent attacks showed. We present our tool DISV (Domain Independent Semantic Validator). It includes a declarative specification language for users to specify semantic properties of a data format. It also includes a validator that takes a data file together with a property specification and checks if the file follows the specification. We demonstrate a rich variety of properties that can be verified by our tool using eight case studies over three data formats. We also demonstrate that our tool can be used to detect advanced attacks on PDF documents.
AB - Data format specification languages such as PDF or HTML have been used extensively for exchanging structured data over the internet. While receivers of data files (e.g., PDF viewers or web browsers) perform syntax validation of files, validating deep semantic properties has not been systematically explored in practice. However, data files that violate semantic properties may cause unintended effects on receivers, such as causing them to crash or creating security breaches, as recent attacks showed. We present our tool DISV (Domain Independent Semantic Validator). It includes a declarative specification language for users to specify semantic properties of a data format. It also includes a validator that takes a data file together with a property specification and checks if the file follows the specification. We demonstrate a rich variety of properties that can be verified by our tool using eight case studies over three data formats. We also demonstrate that our tool can be used to detect advanced attacks on PDF documents.
UR - http://www.scopus.com/inward/record.url?scp=85168769217&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85168769217&partnerID=8YFLogxK
U2 - 10.1109/SPW59333.2023.00020
DO - 10.1109/SPW59333.2023.00020
M3 - Conference contribution
AN - SCOPUS:85168769217
T3 - Proceeding - 44th IEEE Symposium on Security and Privacy Workshops, SPW 2023
SP - 163
EP - 174
BT - Proceeding - 44th IEEE Symposium on Security and Privacy Workshops, SPW 2023
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 22 May 2023 through 25 May 2023
ER -