; This sample code accompanies the the following published work by the same ; authors: ; ; Gilmore R. Lundquist, Vishwath Mohan, and Kevin W. Hamlen. "Searching for ; Software Diversity: Attaining Artificial Diversity through Program ; Synthesis." In Proceedings of the New Security Paradigms Workshop (NSPW), ; 2016. ; ; The code herein is owned by the above authors and The University of Texas at ; Dallas. It is freely usable for research purposes, as long as a citation of ; the above paper is retained with any such usage. All other uses (e.g., ; commercial or proprietary) require the explicit permission of the authors. #lang rosette/safe (define bitwidth 8) (define bv8? (bitvector bitwidth)) (define bv8-const (lambda (v) (bv v bitwidth))) ; model 8-bit registers r1 and r2 (define-symbolic r1 r2 bv8?) ; gadgets are side-effectful; ; use (reset) to clear them. (define r1-symb r1) (define r2-symb r2) (define (reset) (set! r1 r1-symb) (set! r2 r2-symb)) ; G1: r1 *= 2 (define (g1) (set! r1 (bvshl r1 (bv8-const 1)))) ; G2: r2 += 1 (define (g2) (set! r2 (bvadd r2 (bv8-const 1)))) ; G3: r1 -= 1 (define (g3) (set! r1 (bvsub r1 (bv8-const 1)))) ; G4: r1 <- 0 (define (g4) (set! r1 (bv8-const 0))) ; G5: r1 <- 6 (define (g5) (set! r1 (bv8-const 6))) ; G6: r2 <- 1 (define (g6) (set! r2 (bv8-const 1))) ; G7: r1 <- r2 (define (g7) (set! r1 r2)) ; G8: r2 <- r1 (define (g8) (set! r2 r1)) ; given a gadget list, execute each in sequence. (define (run-code code) (map (lambda (g) (g)) code)) ; GOAL: code that produces the result r1 = 4 (define (assert-correct) (assert (equal? r1 (bv8-const 4)))) (define (code-correct code) (reset) (run-code code) (assert-correct)) (require rosette/lib/synthax) ; a grammar for gadget lists (define-synthax (gadget-sequence depth) #:base (list [choose g1 g2 g3 g4 g5 g6 g7 g8]) #:else (cons [choose g1 g2 g3 g4 g5 g6 g7 g8] (gadget-sequence (- depth 1)))) ; a sketch with a hole, to be filled ; with gadget sequences of length 3 (define synthesized-sequence (gadget-sequence 2)) ; synthesize a correct gadget sequence: ; find a concrete model for the symbolic variables ; that satisfies all of our assertions (define soln (synthesize #:forall (list r1 r2) #:guarantee (code-correct synthesized-sequence))) (if (sat? soln) (print-forms soln) (display "Unsatisfiable"))