Design, implementation and formal verification of BGP proxy for mimic router
To ensure the safety and correctness of the critical ‘mimic bracket’ components such as protocol proxies of mimic routers, a BGP (border gateway protocol) proxy was designed and implemented, and formal methods were applied to verify the safety and correctness of the BGP proxy.The BGP packets communi...
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | zho |
| Published: |
Editorial Department of Journal on Communications
2023-03-01
|
| Series: | Tongxin xuebao |
| Subjects: | |
| Online Access: | http://www.joconline.com.cn/zh/article/doi/10.11959/j.issn.1000-436x.2023065/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850096332138610688 |
|---|---|
| author | Jin ZHANG Qiang GE Weihai XU Yiming JIANG Hailong MA Hongtao YU |
| author_facet | Jin ZHANG Qiang GE Weihai XU Yiming JIANG Hailong MA Hongtao YU |
| author_sort | Jin ZHANG |
| collection | DOAJ |
| description | To ensure the safety and correctness of the critical ‘mimic bracket’ components such as protocol proxies of mimic routers, a BGP (border gateway protocol) proxy was designed and implemented, and formal methods were applied to verify the safety and correctness of the BGP proxy.The BGP packets communicated between the peer routers and the master actor were monitored by the BGP proxy.The BGP sessions with the slave actors on behalf of peer routers were established, ensuring the consistency of the BGP protocol states for all actors.The formal specification of the BGP proxy was written based on separation logic.The VeriFast theorem prover was used to prove that the program had no memory safety problems such as null pointer reference.Furthermore, the formal verification of high-level attributes of each module in BGP proxy was also conducted to strictly ensure that the implementation met the specification.The implementation to proof code ratio of BGP proxy is about 1.8:1, and the implementation to proof labor hour ratio is about 1:3.The formally verified BGP proxy consume 0.16 seconds to process 100 000 BGP routes, which is about 7 times as long as the unverified one.Works done provide a reference for applying formal methods to verify the safety and correctness of critical components in mimic defense equipment and systems. |
| format | Article |
| id | doaj-art-c9219d79d0f0418282908bdfdbddbc76 |
| institution | DOAJ |
| issn | 1000-436X |
| language | zho |
| publishDate | 2023-03-01 |
| publisher | Editorial Department of Journal on Communications |
| record_format | Article |
| series | Tongxin xuebao |
| spelling | doaj-art-c9219d79d0f0418282908bdfdbddbc762025-08-20T02:41:14ZzhoEditorial Department of Journal on CommunicationsTongxin xuebao1000-436X2023-03-0144334459387487Design, implementation and formal verification of BGP proxy for mimic routerJin ZHANGQiang GEWeihai XUYiming JIANGHailong MAHongtao YUTo ensure the safety and correctness of the critical ‘mimic bracket’ components such as protocol proxies of mimic routers, a BGP (border gateway protocol) proxy was designed and implemented, and formal methods were applied to verify the safety and correctness of the BGP proxy.The BGP packets communicated between the peer routers and the master actor were monitored by the BGP proxy.The BGP sessions with the slave actors on behalf of peer routers were established, ensuring the consistency of the BGP protocol states for all actors.The formal specification of the BGP proxy was written based on separation logic.The VeriFast theorem prover was used to prove that the program had no memory safety problems such as null pointer reference.Furthermore, the formal verification of high-level attributes of each module in BGP proxy was also conducted to strictly ensure that the implementation met the specification.The implementation to proof code ratio of BGP proxy is about 1.8:1, and the implementation to proof labor hour ratio is about 1:3.The formally verified BGP proxy consume 0.16 seconds to process 100 000 BGP routes, which is about 7 times as long as the unverified one.Works done provide a reference for applying formal methods to verify the safety and correctness of critical components in mimic defense equipment and systems.http://www.joconline.com.cn/zh/article/doi/10.11959/j.issn.1000-436x.2023065/mimic defenseBGProuterformal verification |
| spellingShingle | Jin ZHANG Qiang GE Weihai XU Yiming JIANG Hailong MA Hongtao YU Design, implementation and formal verification of BGP proxy for mimic router Tongxin xuebao mimic defense BGP router formal verification |
| title | Design, implementation and formal verification of BGP proxy for mimic router |
| title_full | Design, implementation and formal verification of BGP proxy for mimic router |
| title_fullStr | Design, implementation and formal verification of BGP proxy for mimic router |
| title_full_unstemmed | Design, implementation and formal verification of BGP proxy for mimic router |
| title_short | Design, implementation and formal verification of BGP proxy for mimic router |
| title_sort | design implementation and formal verification of bgp proxy for mimic router |
| topic | mimic defense BGP router formal verification |
| url | http://www.joconline.com.cn/zh/article/doi/10.11959/j.issn.1000-436x.2023065/ |
| work_keys_str_mv | AT jinzhang designimplementationandformalverificationofbgpproxyformimicrouter AT qiangge designimplementationandformalverificationofbgpproxyformimicrouter AT weihaixu designimplementationandformalverificationofbgpproxyformimicrouter AT yimingjiang designimplementationandformalverificationofbgpproxyformimicrouter AT hailongma designimplementationandformalverificationofbgpproxyformimicrouter AT hongtaoyu designimplementationandformalverificationofbgpproxyformimicrouter |