Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
}
TY - GEN
T1 - Modeling of Checking Program Flow Control Transitions when Executing a Return Instruction
AU - Galimzyanova, Liliya
AU - Porshnev, Sergey
AU - Gilmiyarov, Roman
AU - Syrvacheva, Regina
PY - 2023/5/15
Y1 - 2023/5/15
N2 - Buffer overflow vulnerabilities have been known for a long time, are widespread and relevant today. To protect against buffer overflows, developers of operating systems usually use standard mechanisms of operating systems, but they are not very effective in attacks using return-oriented programming techniques. The article proposes a model for checking the legitimacy of program control flow transitions when executing a return instruction, based on an access graph. The article also provides a model for checking the legitimacy of program control flow transitions when executing a return instruction, based on the use of a shadow stack, a model for generating a program control flow. Modeling was carried out in the specification language based on set theory, first-order logic and temporal logic of actions, models were checked using the Model Checking method. The constructed models can be refined to the required level of abstraction, used to create mechanisms for protecting operating systems based on Linux from attacks using the return-oriented programming technique.
AB - Buffer overflow vulnerabilities have been known for a long time, are widespread and relevant today. To protect against buffer overflows, developers of operating systems usually use standard mechanisms of operating systems, but they are not very effective in attacks using return-oriented programming techniques. The article proposes a model for checking the legitimacy of program control flow transitions when executing a return instruction, based on an access graph. The article also provides a model for checking the legitimacy of program control flow transitions when executing a return instruction, based on the use of a shadow stack, a model for generating a program control flow. Modeling was carried out in the specification language based on set theory, first-order logic and temporal logic of actions, models were checked using the Model Checking method. The constructed models can be refined to the required level of abstraction, used to create mechanisms for protecting operating systems based on Linux from attacks using the return-oriented programming technique.
UR - http://www.scopus.com/inward/record.url?partnerID=8YFLogxK&scp=85164972539
U2 - 10.1109/USBEREIT58508.2023.10158811
DO - 10.1109/USBEREIT58508.2023.10158811
M3 - Conference contribution
SP - 320
EP - 323
BT - Proceedings - 2023 IEEE Ural-Siberian Conference on Biomedical Engineering, Radioelectronics and Information Technology, USBEREIT 2023
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 2023 IEEE Ural-Siberian Conference on Biomedical Engineering, Radioelectronics and Information Technology (USBEREIT)
Y2 - 15 May 2023 through 17 May 2023
ER -
ID: 41985005