How Inadequate Specification, Buggy Implementation, and Deficient Platform-Support Hinder Security

ABSTRACT

Developing a secure system (or, protocol) in general boils down to having a correct and robust specification which developers faithfully implement with the available platform support. Vulnerabilities can thus crop up due to inadequate specification, buggy implementations, or the lack of appropriate security constructs in the platform. In this talk, I will present examples of insecurity due to inadequate specification, wrong implementations, and deficient platform support. I will particularly focus on how automated reasoning and formal verification techniques can greatly contribute towards detecting vulnerabilities. In the first example, I will show how 4G LTE telecommunication protocol specification lacks security considerations which can be exploited by adversaries to have catastrophic impacts. Next, I will present how incorrect X.509 certificate validation implementations in open-source SSL/TLS libraries leave users prone to impersonation attacks. Finally, I will conclude my talk with a discussion of how lack of hardware support makes enforcing Digital Rights Management (DRM) policies infeasible for mobile devices.

References

1. S. Y. Chau, O. Chowdhury, E. Hoque, H. Ge, A. Kate, C. Nita-Rotaru, and N. Li. 2017. SymCerts: Practical Symbolic Execution for Exposing Noncompliance in X.509 Certificate Validation Implementations. In 2017 IEEE Symposium on Security and Privacy (SP). 503--520.
2. Syed Rafiul Hussain, Omar Chowdhury, Shagufta Mehnaz, and Elisa Bertino. 2018. LTEInspector: A Systematic Approach for Adversarial Testing of 4G LTE 2018 Network and Distributed System Security Symposium (NDSS).

Index Terms

• Security and privacy

  • Formal methods and theory of security

    • Logic and verification

  • Network security

    • Mobile and wireless security

    • Security protocols

  • Systems security

    • Operating systems security

      • Mobile platform security