Iotverif: Automatic Verification of SSL/TLS Certificate for IoT Applications

被引:4
作者
Liu, Anyi [1 ]
Alqazzaz, Ali [2 ]
Ming, Hua [1 ]
Dharmalingam, Balakrishnan [1 ]
机构
[1] Oakland Univ, Dept Comp Sci & Engn, Rochester, MI 48309 USA
[2] Univ Bisha, Bisha 67714, Saudi Arabia
基金
美国国家科学基金会;
关键词
Internet of Things; Protocols; Security; Servers; Software; Payloads; Sockets; Certificate; Internet of Things (IoT); model checking; protocol verification; secure socket layer (SSL); transport layer security (TLS); PROTOCOL VERIFICATION; SECURITY;
D O I
10.1109/ACCESS.2019.2961918
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Although extensive research has been conducted on securing the Internet of Things (IoT) communication protocols, various vulnerabilities and exploits are continuously discovered and reported. Since vulnerabilities are introduced from either insecure communication protocols or defectiveness of applications, it is difficult to identify them during the software development or testing phase. In this paper, we present IoTVerif, a system that automatically verifies the Secure Socket Layer/Transport Layer Security (SSL/TLS) certificate for IoT applications that utilize broker-based messaging protocols. IoTVerif constructs the specification of an IoT protocol and verifies its security properties, without relying on prior knowledge about communication protocols. Once the specification is constructed, a general-purpose model checker automatically verifies those properties, as well as generates counter-examples if any property does not hold. We analyze the effectiveness of IoTVerif with real-world IoT-related applications. Our evaluation results show that IoTVerif can successfully identify vulnerabilities from IoT applications, which are exploitable by the man-in-the-middle (MITM) and TLS renegotiation attacks. IoTVerif holds a great promise for reverse-engineering emerging IoT messaging protocols and identifies the vulnerabilities from IoT-related applications.
引用
收藏
页码:27038 / 27050
页数:13
相关论文
共 71 条
  • [1] Analyzing security protocols with secrecy types and logic programs
    Abadi, M
    Blanchet, B
    [J]. JOURNAL OF THE ACM, 2005, 52 (01) : 102 - 146
  • [2] Akdeniz, 2017, GOOGL PLAY CRAWL
  • [3] Lucky Thirteen: Breaking the TLS and DTLS Record Protocols
    AlFardan, Nadhem J.
    Paterson, Kenneth G.
    [J]. 2013 IEEE SYMPOSIUM ON SECURITY AND PRIVACY (SP), 2013, : 526 - 540
  • [4] IoTVerif: An Automated Tool to Verify SSL/TLS Certificate Validation in Android MQTT Client Applications
    Alghamdi, Khalid
    Alqazzaz, Ali
    Liu, Anyi
    Ming, Hua
    [J]. PROCEEDINGS OF THE EIGHTH ACM CONFERENCE ON DATA AND APPLICATION SECURITY AND PRIVACY (CODASPY'18), 2018, : 95 - 102
  • [5] AspectDroid: Android App Analysis System
    Ali-Gombe, Aisha
    Ahmed, Irfan
    Richard, Golden G., III
    Roussev, Vassil
    [J]. CODASPY'16: PROCEEDINGS OF THE SIXTH ACM CONFERENCE ON DATA AND APPLICATION SECURITY AND PRIVACY, 2016, : 145 - 147
  • [6] Amalfitano D, 2012, IEEE INT CONF AUTOM, P258, DOI 10.1145/2351676.2351717
  • [7] Amazon Inc, AMAZ APPST
  • [8] Amazon Web Services, 2017, CLOUDMQTT GLOB DISTR
  • [9] Anand S., 2012, MATER SCI FORUM
  • [10] Android Studio, 2017, UI APPL EX MONK