Security types in Racket

security-types.rkt

#lang typed/racket

;; Types ---------------------------------
(struct: (a) High ([v : a]))              ; a wrapper for high security objects
(struct: (a) Low ([v : a]))               ; a wrapper for low security objects
(define-type (ST a) (U (High a) (Low a))) ; a type that can be used for either high or low

;; allows us to get the value of the object regardless of the type (reduces duplication)
(: ST-v (All (A) ((ST A) -> A)))
(define (ST-v a)
  (cond [(Low? a)  (Low-v a)]
        [(High? a) (High-v a)]))

(: upgrade-security (All (A) ((ST A) -> (High A))))
(define (upgrade-security a)
   (cond [(Low? a) (High (Low-v a))]
         [(High? a) a]))

;; encryption functions --------------------------------
(: rot13-char (Char -> Char))
(define (rot13-char ch)
  (let* ([b (char->integer ch)]
         [a (if (< b 96) 65 97)])
    (integer->char (+ (modulo (+ 13 (- b a)) 26) a))))

(: rot13 (String -> String))
(define (rot13 str)
  (list->string (map rot13-char (string->list str))))

;; functions that apply security constraints -----------

(: risky ((ST String) -> (ST String)))
(define (risky a)
  ; pretend something risky happens here, like reading confidential data 
  (upgrade-security a))

(: encrypt ((ST String) -> (Low String)))
(define (encrypt a)
  ; any confidential data becomes unreadable
  (Low (rot13 (ST-v a))))

(: public-channel ((Low String) -> Void))
(define (public-channel a)
  ; Only allows low-security items to be output
  (display (ST-v a)))

;; Examples -------------------------------

(ST-v (risky (Low "H")))    ; Low security input, high security output
(ST-v (risky (High "I")))   ; High security input, high security output

; public channel will only allow low-security output
(public-channel (High "Hello there"))              ; Disallowed at compile time (type-error)
(public-channel (encrypt (High "Hello there")))    ; Allowed