Sökning: id:"swepub:oai:research.chalmers.se:b05530f1-a0a0-4b5a-af17-2738a5d97924" >
Short Paper: Weak R...
Short Paper: Weak Runtime-Irrelevant Typing for Security
-
- Gissurarson, Matthías Páll, 1991 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Mista, Claudio Agustin, 1991 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
(creator_code:org_t)
- 2020-11-09
- 2020
- Engelska.
-
Ingår i: PLAS 2020 - Proceedings of the 15th Workshop on Programming Languages and Analysis for Security. - New York, NY, USA : ACM. ; , s. 13-17
- Relaterad länk:
-
https://research.cha...
-
visa fler...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- Types indexed with extra type-level information are a powerful tool for statically enforcing domain-specific security properties. In many cases, this extra information is runtime-irrelevant, and so it can be completely erased at compile-time without degrading the performance of the compiled code. In practice, however, the added bureaucracy often disrupts the development process, as programmers must completely adhere to new complex constraints in order to even compile their code. In this work we present WRIT, a plugin for the GHC Haskell compiler that relaxes the type checking process in the presence of runtime-irrelevant constraints. In particular, WRIT can automatically coerce between runtime equivalent types, allowing users to run programs even in the presence of some classes of type errors. This allows us to gradually secure our code while still being able to compile at each step, separating security concerns from functional correctness. Moreover, we present a novel way to specify which types should be considered equivalent for the purpose of allowing the program to run, how ambiguity at the type level should be resolved and which constraints can be safely ignored and turned into warnings.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datorteknik (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Engineering (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)
Nyckelord
- haskell
- type checking
- ghc
- compilers
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)