3 Homework 3
Released: Wednesday, January 25, 2023 at 6:00pm
Due: Wednesday, February 1, 2023 at 6:00pm
What to Download:
Please start with this file, filling in where appropriate, and submit your homework to the HW3 assignment on Gradescope. This page has additional information, and allows us to format things nicely.
NOTE: You need to update ISL-Spec to complete this assignment. You will get errors related to the third problem if you do not. Go to File->Install Package, type in "isl-spec" and click "Update".
3.1 Problem 1
Cryptography, or the science of secret communication, is about as old as math itself. Modern cryptography was born alongside with computers, as during WWII, information was sent over radio and secure communication was critical. Machines were used in what became an arms race, where more sophisticated codes were developed using complex machinery, and at the same time, some of the earliest "computers" were created in order to break them.
One of the first, and most important, cryptanalysis (code breaking) results was done by teams at Bletchley Park, a British estate that housed one of the first machines that could conceivably be called the computer. While many were involved in the effort, including a team of Polish mathematicians, a key figure in the effort was a British mathematician and one of the pioneers of the entire field of computer science named Alan Turing. For his contributions to this early work on computation, and many other things, the highest award in computer science (our "Nobel Prize") is named the Turing award.
Despite his critical role in the effort, and ground breaking work for the field as a whole, Turing was prosecuted for homosexuality after the war, and died by apparent suicide a few years later at the age of only 41. More than a half century later, the British Government appologized for his treatment and officially pardoned him.
Much of cryptanalysis relies upon detecting patterns, and indeed, the ability to do that at scale was exactly how the Bletchley Park team was able to use machines to break the German Enigma.
"Perfect encryption" via so-called one-time pads, or the other hand, has no patterns, and thus is not vulnerable to that type of analysis, even in theory. It is, in effect, unbreakable. It relies, on the other hand, on a secret key, shared beforehand, that is as long as the message itself, which aside from limited cases, is difficult to imagine (the "Red Telephone" in movies between the US and USSR is fiction, but keys to enable this form of encryption were exchanged via embassies). Most modern cryptography, on the other hand, relies upon being able to negotiate secure communication between parties that have never interacted before (you and an online shopping website, for example).
One-time pads, however, still do have value, in that they are provably impossible to break, and we will show why that is in this problem. Further, most realistic cryptosystems, while much more complex, share elements with this incredibly simple one.
First, we will define types for bits, messages (of fixed length of six bits), and keys (of fixed length of six bits). In a realistic setting, we could translate text into bits (each letter getting a unique assignment of bits), and split our message into chunks of length six. We define generators for Bit and Message.
; A Bit is one of:
; - 0
; - 1
(define Bit (qc:choose-one-of (list 0 1)))
; A Key is a (list Bit Bit Bit Bit Bit Bit)
(define Key (qc:choose-list Bit 6))
; A Message is a (list Bit Bit Bit Bit Bit Bit)
(define Message (qc:choose-list Bit 6))
The way one-time pads work is via exclusive-or (XOR). To both encrypt and decrypt, we XOR each bit in the message with a corresponding bit in the key. This should result in an encrypted message for which it is impossible to determine the original without knowing the key. We want to prove that, and we’ll do it in the following way. First, we define encryption and decryption, which use the key (which is the same length of the message), XOR’d bit by bit with the message:
; xor : Bit Bit -> Bit
(define (xor b1 b2)
(modulo (+ b1 b2) 2))
(check-expect (xor 0 0) 0)
(check-expect (xor 0 1) 1)
(check-expect (xor 1 0) 1)
(check-expect (xor 1 1) 0)
; xor-list : [List-of Bit] [List-of Bit] -> [List-of Bit]
(define (xor-list l1 l2)
(map xor l1 l2))
(check-expect (xor-list (list 1 0 0) (list 1 1 1)) (list 0 1 1))
(check-expect (xor-list (list 0 0 0) (list 0 0 0)) (list 0 0 0))
; encrypt : Message Key -> Message
(define encrypt xor-list)
; decrypt : Message Key -> Message
(define decrypt xor-list)
Your task is to define the following property, that captures the fact that encrypt/decrypt result in perfect secrecy. It should state that for a given encrypted message, for any possible original message, there exists some key that would have produced it. That means that without knowing something about the key, there is no way of knowing which message was encrypted, since for any message, some key could have produced the encrypted message. Note that we don’t have a logical exists (\exists), but if you can compute such a key, that is essentially the same thing (to be more technical, it’s very close to an existential in constructive logic). To show that you have, indeed, computed the right key, your property should finally use it to decrypt the message.
(define (xor-perfect-prop encr-msg) ...)
(check-property (for-all [(x Message)] (xor-perfect-prop x)))
3.2 Problem 2
Many cities have a problem with landlords who own many properties but do not adequately maintain them. In some, there are people who have begun organizing "tenants unions" to combat this, and an important way they can work is to organize together between buildings that are owned by the same landlord.
For a landlord with hundreds of properties, a single building threatening to withhold rent is perhaps easily ignored or addressed with evictions, but if many buildings do it, such "rent strikes" become a much bigger problem. For the organizers, identifying such landlords can be difficult, since the buildings are often owned by shell companies in order to hide true ownership (1 Main St might be owned by "1 Main St LLC").
One way to identify these landlords is to look at the addresses for company registrations, as while creating companies to own buildings is usually relatively easy, organizing them usually requires having centralized management, and thus, the same business address for all the shell companies.
(define-struct tax-record [address value owner])
;; A TaxRecord is a (make-tax-record String Number String)
(define-struct building-owner [name address])
;; A BuildingOwner is a (make-building-owner String String)
;; Invariant: name is globally unique.
(define-struct owner-assets [names assets])
;; An OwnerAssets is a (make-owner-assets [List-of String] Number)
; find-landlords: [List-of TaxRecord] [List-of BuildingOwner] -> [List-of OwnerAssets]
; find mega-landlords by using the addresses of owners to merge ostensibly different landlords,
; totalling the assets for each unique address
(define (find-landlords tr bor) ...)
Your task is to write a correctness spec for the function find-landlords that takes a list of TaxRecords and a list of BuildingOwners, and computes a list of OwnerAssets, merging differently named BuildingOwners that share an address. The function will combine the total value of all the buildings owned by the owners that share the same company registration address, storing that total dollar amount, along with the owner names, in the OwnerAssets.
As an example, consider the following input and output:
(find-landlords (list (make-tax-record "1 Main St" 100000 "1 Main St, LLC")
(make-tax-record "2 Main St" 150000 "2 Main St, LLC")
(make-tax-record "3 Main St" 110000 "Alex Anderson")
(make-tax-record "4 Main St" 120000 "Great Properties LLC")
(make-tax-record "5 Main St" 100000 "Great Properties LLC"))
(list (make-building-owner "1 Main St, LLC" "1 Business Place")
(make-building-owner "2 Main St, LLC" "1 Business Place")
(make-building-owner "Alex Anderson" "3 Main St")
(make-building-owner "Great Properties LLC" "2 Business Place")))
; => (list (make-owner-assets (list "1 Main St, LLC" "2 Main St, LLC") 250000)
; (make-owner-assets (list "Alex Anderson") 110000)
; (make-owner-assets (list "Great Properties LLC") 220000))
The spec should capture properties that relate the output of find-landlords (which you do not have to implement, though are welcome to) with the inputs. Think about how to ensure that any implementation of find-landlords that satisfies your spec does the right thing. You might want to think about the relationship of money between the input and the output, about how to ensure duplication hasn’t happened, how to ensure properties were combined properly, etc.
;; find-landlords-spec : [List-of TaxRecord] [List-of BuildingOwner] -> Boolean
(define (find-landlords-spec tr bor)
...)
3.3 Problem 3
One key source of cybersecurity vulnerabilities are "timing attacks", which work by measuring how long a particular computation takes. If the computation takes different amount of time based on different secret values, the attacker may be able to learn information about those secrets.
In this problem, we’ll consider one of the classic examples of this: matching passwords.
Since recording precise timing can be tricky (and may require collecting many samples), we’ll simulate the timing by using a fake clock that we move forward with a tick! function, and define versions of functions that call this explicitly.
You must use these functions if you need their functionality, rather than built-in versions (or re-implementing them without the calls to tick!), as the built-in versions are fast enough that without significant sampling, the timing results we would get (using, e.g., a call to get the current clock time before and after a function runs) won’t be consistent. Note that in real attacks, extremely small differences of timing are enough (as statistically they become significant), so this constraint exists only to make the assignment straightforward.
; tick-string=? : String String -> Bool
(define (tick-string=? s1 s2)
(local [(define ticks (min (string-length s1)
(string-length s2)))
(define _ (build-list ticks (λ(_) (tick!))))]
(string=? s1 s2)))
; tick-length : (X) [List-of X] -> Number
(define (tick-length l)
(local [(define _ (tick!))]
(cond [(empty? l) 0]
[(cons? l) (+ 1 (tick-length (rest l)))])))
You’ve been given a function check-password that takes as input a list of characters (as strings) and checks in against a password (stored as a constant). It does it by using a list=? helper that calls the tick-string=? function on each letter.
; list=? : (X) [X -> Bool] [List-of X] [List-of X] -> Bool
(define (list=? elt=? l1 l2)
(cond [(and (empty? l1) (empty? l2)) #t]
[(and (empty? l1) (cons? l2)) #f]
[(and (cons? l1) (empty? l2)) #f]
[(and (cons? l1) (cons? l2))
(and (elt=? (first l1) (first l2))
(list=? elt=? (rest l1) (rest l2)))]))
(define PASSWORD (explode "a7he29hdee"))
; check-password : [List-of String] -> Bool
(define (check-password p)
(list=? tick-string=? PASSWORD p))
You have two tasks. First, you need to write a specification that ensures that check-password does not leak timing information. For this, you should use the start-timer! function, provided by ISL-Spec, to reset the simulated clock before calling check-password, and then call get-timer! to get the clock value (a natural number) after the call. You should do this for two passwords, and ensure that each takes exactly the same number of ticks.
(define (timing-spec p1 p2)
...)
(check-property (for-all [(p1 String)
(p2 String)]
(timing-spec p1 p2)))
Once you have that spec, you should find that the implementation of check-password is indeed leaking timing information. An attacker could use that to guess the password, as the current implementation stops as soon as it finds a character that doesn’t match, so they could try passwords starting with "a", then "b", etc, until they found one that took a little longer: this would mean they discovered the first letter. Then they would continue with the second, etc. You can try this out (but don’t have to) by trying check-password with passwords that are longer and longer prefixes of the actual password.
Your next task is to go back and fix the implementation of check-password to not reveal that information.
There may be multiple ways to do this; the only requirement is that it no longer fails your timing specification, and you are not allowed to use either string=? or length (or to re-implement) them yourself, but rather must use the provided versions that invoke tick!. Similarly, you cannot use equal? as a way around using tick-string=?. Failure to follow those instructions will result in a 0 on this part of the problem. Note that you can have your functions call tick! themselves, in order to balance out the cost of other calls. This may correspond to doing pointless work, which is indeed an important element of this type of security!
Note: you may not reset the clock (by calling start-timer!) after you compare passwords but before you look at the clock with get-timer!. This amounts to ignoring the timing results entirely (you might as well just assert 0 = 0), and would not be a valid solution.