research-article

Towards secure IoT programming in Haskell

Authors:

Nachiappan Valliappan,

Alejandro Russo,

Koen ClaessenAuthors Info & Claims

Haskell 2020: Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell

Pages 136 - 150

https://doi.org/10.1145/3406088.3409027

Published: 09 August 2020 Publication History

Abstract

IoT applications are often developed in programming languages with low-level abstractions, where a seemingly innocent mistake might lead to severe security vulnerabilities. Current IoT development tools make it hard to identify these vulnerabilities as they do not provide end-to-end guarantees about how data flows within and between appliances. In this work we present Haski, an embedded domain specific language in Haskell (eDSL) for secure programming of IoT devices. Haski enables developers to write Haskell programs that generate C code without falling into many of C’s pitfalls. Haski is designed after the synchronous programming language Lustre, and sports a backwards compatible information-flow control extension to restrict how sensitive data is propagated and modified within the application. We present a novel eDSL design which uses recursive monadic bindings and allows a natural use of functions and pattern-matching in Haskell to write Haski programs. To showcase Haski, we implement a simple smart house controller where communication is done via low-energy Bluetooth on Zephyr OS.

Supplemental Material

MP4 File

Presentation Videos

Download
42.11 MB

References

[1]

Cédric Auger, J. L. Colaco, Grégoire Hamon, and Marc Pouzet. 2012. A Formalization and Proof of a Modular Lustre Compiler.

[2]

Emil Axelsson, Koen Claessen, Gergely Dévai, Zoltán Horváth, Karin Keijzer, Bo Lyckegård, Anders Persson, Mary Sheeran, Josef Svenningsson, and András Vajda. 2010. Feldspar: A domain specific language for digital signal processing algorithms. In 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010 ). 169-178.

Digital Library

[3]

Patrick Bahr, Christian Graulund, and Rasmus Ejlers Møgelberg. 2019. Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks. Proc. ACM Program. Lang. 3, ICFP ( 2019 ).

Digital Library

[4]

David E. Bell and L. La Padula. 1976. Secure Computer System: Unified Exposition and Multics Interpretation. Technical Report MTR-2997, Rev. 1. MITRE Corporation, Bedford, MA.

[5]

Elisa Bertino and Nayeem Islam. 2017. Botnets and Internet of Things Security. IEEE Computer 50, 2 ( 2017 ), 76-79.

Digital Library

[6]

Dariusz Biernacki, Jean-Louis Colaço, Gregoire Hamon, and Marc Pouzet. 2008. Clock-directed modular code generation for synchronous data-flow languages. In Proceedings of the 2008 ACM SIGPLAN-SIGBED conference on Languages, compilers, and tools for embedded systems. 121-130.

Digital Library

[7]

Per Bjesse, Koen Claessen, Mary Sheeran, and Satnam Singh. 1998. Lava: Hardware Design in Haskell. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP '98).

Digital Library

[8]

Timothy Bourke, Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet, and Lionel Rieg. 2017. A formally verified compiler for Lustre. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. 586-601.

Digital Library

[9]

Pablo Buiras, Deian Stefan, and Alejandro Russo. 2014. On Dynamic FlowSensitive Floating-Label Systems. In IEEE Computer Security Foundations Symposium, CSF. 65-79.

[10]

P. Buiras, D. Vytiniotis, and A. Russo. 2015. HLIO: Mixing Static and Dynamic Typing for Information-Flow Control in Haskell. In Proc. of the ACM SIGPLAN International Conference on Functional Programming (ICFP '15). ACM.

[11]

Paul Caspi, Grégoire Hamon, and Marc Pouzet. 2008. Synchronous functional programming: The lucid synchrone experiment. Real-Time Systems: Description and Verification Techniques: Theory and Tools. Hermes ( 2008 ), 28-41.

[12]

Paul Caspi, Daniel Pilaud, Nicolas Halbwachs, and John Plaice. 1987. Lustre: A Declarative Language for Programming Synchronous Systems. In Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages.

[13]

Z. Berkay Celik, Leonardo Babun, Amit Kumar Sikder, Hidayet Aksu, Gang Tan, Patrick D. McDaniel, and A. Selcuk Uluagac. 2018. Sensitive Information Tracking in Commodity IoT. In USENIX Security.

[14]

Antony Courtney, Henrik Nilsson, and John Peterson. 2003. The Yampa arcade. In Proc. of the ACM SIGPLAN Workshop on Haskell. 7-18.

Digital Library

[15]

D. E. Denning and P. J. Denning. 1977. Certification of Programs for Secure Information Flow. Commun. ACM 20, 7 ( July 1977 ), 504-513.

[16]

Conal Elliott and Paul Hudak. 1997. Functional Reactive Animation. In Proc. of the ACM SIGPLAN International Conference on Functional Programming. 263-273.

Digital Library

[17]

Trevor Elliott, Lee Pike, Simon Winwood, Patrick C. Hickey, James Bielman, Jamey Sharp, Eric L. Seidel, and John Launchbury. 2015. Guilt free ivory. In Proc. of the ACM SIGPLAN Symposium on Haskell. 189-200.

Digital Library

[18]

Earlence Fernandes, Jaeyeon Jung, and Atul Prakash. 2016. Security Analysis of Emerging Smart Home Applications. In IEEE Symposium on Security and Privacy, SP. 636-654.

[19]

Mark Grebe and Andy Gill. 2016. Threading the Arduino with Haskell. In Trends in Functional Programming-17th International Conference, TFP. 135-154.

[20]

Nicholas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud. 1991. The synchronous data flow programming language LUSTRE. Proc. IEEE 79, 9 ( 1991 ), 1305-1320.

[21]

P. Hawkins, A. Aiken, K. Fisher, M. Rinard, and M. Sagiv. 2011. Data Representation Synthesis. In Proc. ACM Conference on Programming Language Design and Implementation.

[22]

Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. 1993. Partial Evaluation and Automatic Program Generation. Prentice-Hall, Inc., USA.

Digital Library

[23]

Marcela S. Melara, David H. Liu, and Michael J. Freedman. 2019. Pyronia: Redesigning Least Privilege and Isolation for the Age of IoT. CoRR abs/ 1903. 01950 ( 2019 ). arXiv: 1903. 01950 htp://arxiv.org/abs/ 1903.01950

[24]

Agustin Mista and Alejandro Russo. 2020. BinderAnn: Automated Reification of Source Annotations for Monadic EDSLs. In 21st International Symposium on Trends in Functional Programming, TFP.

[25]

Shayan Najd and Simon Peyton Jones. 2017. Trees that Grow. Journal of Universal Computer Science 23, 1 ( 2017 ), 42-62.

[26]

Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geofrey Washburn. 2006. Simple unification-based type inference for GADTs. In Proc. of the ACM SIGPLAN International Conference on Functional Programming, ICFP.

Digital Library

[27]

Matthew Pickering, Gergo Érdi, Simon Peyton Jones, and Richard A. Eisenberg. 2016. Pattern synonyms. In Proc. of the 9th International Symposium on Haskell, Haskell 2016.

[28]

Lee Pike, Nis Wegmann, Sebastian Niller, and Alwyn Goodloe. 2013. Copilot: monitoring embedded systems. ISSE 9, 4 ( 2013 ), 235-255.

[29]

Jie Qian, Jing Liu, Xiang Chen, and Junfeng Sun. 2015. Modeling and Verification of Zone Controller: The SCADE Experience in China's Railway Systems. In 1st IEEE/ACM International Workshop on Complex Faults and Failures in Large Software Systems, COUFLESS 2015. 48-54.

Digital Library

[30]

Vineet Rajani and Deepak Garg. 2018. Types for information flow control: Labeling granularity and semantic models. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). IEEE, 233-246.

[31]

A. Russo. 2015. Functional Pearl: Two Can Keep a Secret, if One of Them Uses Haskell. In Proc. of the ACM SIGPLAN International Conference on Functional Programming (ICFP 2015 ). ACM.

Digital Library

[32]

A. Russo, K. Claessen, and J. Hughes. 2008. A library for light-weight information-flow security in Haskell. In Proc. ACM SIGPLAN symposium on Haskell (HASKELL '08). ACM.

[33]

A. Sabelfeld and A. C. Myers. 2003. Language-Based Information-Flow Security. IEEE J. Selected Areas in Communications 21, 1 (Jan. 2003 ), 5-19.

Digital Library

[34]

Roei Schuster, Vitaly Shmatikov, and Eran Tromer. 2018. Situational Access Control in the Internet of Things. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS.

Digital Library

[35]

D. Stefan, A. Russo, D. Mazières, and J. C. Mitchell. 2011a. Disjunction Category Labels. In Proc. of the Nordic Conference on Information Security Technology for Applications (NORDSEC '11). Springer-Verlag.

[36]

D. Stefan, A. Russo, J. C. Mitchell, and D. Mazières. 2011b. Flexible Dynamic Information Flow Control in Haskell. In Proc. of the ACM SIGPLAN Haskell symposium (HASKELL '11).

[37]

Nicolas Tsiftes and Thiemo Voigt. 2018. Velox VM : A safe execution environment for resource-constrained IoT applications. J. Netw. Comput. Appl. 118 ( 2018 ).

[38]

Atze van der Ploeg and Koen Claessen. 2015. Practical principled FRP: forget the past, change the future, FRPNow!. In Proc. of the ACM SIGPLAN International Conference on Functional Programming, ICFP. 302-314.

Digital Library

[39]

Qi Wang, Wajih Ul Hassan, Adam Bates, and Carl A. Gunter. 2018. Fear and Logging in the Internet of Things. In 25th Annual Network and Distributed System Security Symposium, NDSS.

[40]

Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhães. 2012. Giving Haskell a Promotion. In Proc. of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI '12). ACM.

Digital Library

Cited By

Li STrinder PDe Troyer CLubbers MRamsingh AFernandez-Reyes KVoinea A(2024)The Benefits of Tierless Elixir/Potato for Engineering IoT SystemsProceedings of the 23rd ACM SIGPLAN International Workshop on Erlang10.1145/3677995.3678197(84-95)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3677995.3678197
Pettersson MLjung Ekeroth JRusso A(2023)Calculating Function Sensitivity for Synthetic Data AlgorithmsProceedings of the 35th Symposium on Implementation and Application of Functional Languages10.1145/3652561.3652567(1-12)Online publication date: 29-Aug-2023
https://dl.acm.org/doi/10.1145/3652561.3652567
Hui JEdwards S(2023)Towards Sparse Synchronous Programming in LuaProceedings of Cyber-Physical Systems and Internet of Things Week 202310.1145/3576914.3587502(361-366)Online publication date: 9-May-2023
https://dl.acm.org/doi/10.1145/3576914.3587502
Show More Cited By

Index Terms

Towards secure IoT programming in Haskell
1. Security and privacy
  1. Systems security
    1. Information flow control
2. Software and its engineering
  1. Software notations and tools
    1. Context specific languages
      1. Domain specific languages

Recommendations

Rewriting a shallow DSL using a GHC compiler extension
GPCE 2017: Proceedings of the 16th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences

Embedded Domain Specific Languages are a powerful tool for developing customized languages to fit specific problem domains. Shallow EDSLs allow a programmer to program using many of the features of a host language and its syntax, but sacrifice ...
The Intel labs Haskell research compiler
Haskell '13

The Glasgow Haskell Compiler (GHC) is a well supported optimizing compiler for the Haskell programming language, along with its own extensions to the language and libraries. Haskell's lazy semantics imposes a runtime model which is in general difficult ...
Rewriting a shallow DSL using a GHC compiler extension
GPCE '17

Embedded Domain Specific Languages are a powerful tool for developing customized languages to fit specific problem domains. Shallow EDSLs allow a programmer to program using many of the features of a host language and its syntax, but sacrifice ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

Haskell 2020: Proceedings of the 13th ACM SIGPLAN International Symposium on Haskell

August 2020

150 pages

ISBN:9781450380508

DOI:10.1145/3406088

General Chair:
Tom Schrijvers

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 August 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Available / v1.1

Author Tags

Qualifiers

Research-article

Funding Sources

Vetenskapsrådet
Stiftelsen för Strategisk Forskning

Conference

ICFP '20

Sponsor:

SIGPLAN

ICFP '20: ACM SIGPLAN International Conference on Functional Programming

August 27, 2020

Virtual Event, USA

Acceptance Rates

Overall Acceptance Rate 57 of 143 submissions, 40%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
445
Total Downloads

Downloads (Last 12 months)34
Downloads (Last 6 weeks)6

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Li STrinder PDe Troyer CLubbers MRamsingh AFernandez-Reyes KVoinea A(2024)The Benefits of Tierless Elixir/Potato for Engineering IoT SystemsProceedings of the 23rd ACM SIGPLAN International Workshop on Erlang10.1145/3677995.3678197(84-95)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3677995.3678197
Pettersson MLjung Ekeroth JRusso A(2023)Calculating Function Sensitivity for Synthetic Data AlgorithmsProceedings of the 35th Symposium on Implementation and Application of Functional Languages10.1145/3652561.3652567(1-12)Online publication date: 29-Aug-2023
https://dl.acm.org/doi/10.1145/3652561.3652567
Hui JEdwards S(2023)Towards Sparse Synchronous Programming in LuaProceedings of Cyber-Physical Systems and Internet of Things Week 202310.1145/3576914.3587502(361-366)Online publication date: 9-May-2023
https://dl.acm.org/doi/10.1145/3576914.3587502
Lubbers MKoopman PRamsingh ASinger JTrinder P(2023)Could Tierless Languages Reduce IoT Development Grief?ACM Transactions on Internet of Things10.1145/35729014:1(1-35)Online publication date: 23-Feb-2023
https://dl.acm.org/doi/10.1145/3572901
Krook RHui JSvensson BEdwards SClaessen K(2022)Creating a Language for Writing Real-Time Applications for the Internet of Things2022 20th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)10.1109/MEMOCODE57689.2022.9954383(1-20)Online publication date: 13-Oct-2022
https://doi.org/10.1109/MEMOCODE57689.2022.9954383
Crooijmans SLubbers MKoopman P(2022)Reducing the Power Consumption of IoT with Task-Oriented ProgrammingTrends in Functional Programming10.1007/978-3-031-21314-4_5(80-99)Online publication date: 17-Mar-2022
https://dl.acm.org/doi/10.1007/978-3-031-21314-4_5
Bocu RBocu D(2022)Conceptual Foundations of Code Rationalization Through a Case Study in HaskellAdvanced Information Networking and Applications10.1007/978-3-030-99584-3_11(116-128)Online publication date: 31-Mar-2022
https://doi.org/10.1007/978-3-030-99584-3_11
Valliappan NRusso ALindley SHage J(2021)Practical normalization by evaluation for EDSLsProceedings of the 14th ACM SIGPLAN International Symposium on Haskell10.1145/3471874.3472983(56-70)Online publication date: 18-Aug-2021
https://dl.acm.org/doi/10.1145/3471874.3472983

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents