Recently, news broke about a new possible offline attack on WPA2 using PMKID. To summarize the attack, WPA2 protected APs can end up broadcasting PMKID values which can then be used to offline-brute-force the password.
These PMKID values are computed this way:
PMKID = HMAC-SHA1-128(PMK, "PMK Name" | MAC_AP | MAC_STA)
| defmodule HiPE.Loader do | |
| @doc "Returns `module_info`s for all loaded modules, with `native: true|false`" | |
| def all_modules(native \\ false) do | |
| :code.all_loaded() | |
| |> Enum.map(&elem(&1, 0)) | |
| |> Enum.map(&Kernel.apply(&1, :module_info, [])) | |
| |> Enum.map(&Enum.into(&1, %{})) | |
| |> Enum.filter(fn %{compile: compile} -> | |
| !match?([], compile) | |
| end) |
why doesn't radfft support AVX on PC?
So there's two separate issues here: using instructions added in AVX and using 256-bit wide vectors. The former turns out to be much easier than the latter for our use case.
Problem number 1 was that you positively need to put AVX code in a separate file with different compiler settings (/arch:AVX for VC++, -mavx for GCC/Clang) that make all SSE code emitted also use VEX encoding, and at the time radfft was written there was no way in CDep to set compiler flags for just one file, just for the overall build.
[There's the GCC "target" annotations on individual funcs, which in principle fix this, but I ran into nasty problems with this for several compiler versions, and VC++ has no equivalent, so we're not currently using that and just sticking with different compilation units.]
The other issue is to do with CPU power management.
| -- Note: There is a more complete explanation at https://github.com/hwayne/lets-prove-leftpad/tree/master/idris | |
| import Data.Vect | |
| -- `minus` is saturating subtraction, so this works like we want it to | |
| eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k | |
| eq_max n Z = rewrite minusZeroRight n in rewrite plusZeroRightNeutral n in Refl | |
| eq_max Z (S _) = Refl | |
| eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl | |
| -- The type here says "the result is" padded to (maximum k n), and is padding plus the original |
| // Copyright 2018 Google LLC | |
| // | |
| // Licensed under the Apache License, Version 2.0 (the "License"); | |
| // you may not use this file except in compliance with the License. | |
| // You may obtain a copy of the License at | |
| // | |
| // http://www.apache.org/licenses/LICENSE-2.0 | |
| // | |
| // Unless required by applicable law or agreed to in writing, software | |
| // distributed under the License is distributed on an "AS IS" BASIS, |
| open FStar.Char | |
| open FStar.Seq | |
| (* Helper *) | |
| let max a b = if a > b then a else b | |
| (* Definition *) | |
| let leftpad (c:char) (n:nat) (s:seq char) : seq char = | |
| let pad = max (n - length s) 0 in | |
| append (create pad c) s |
| theory Leftpad | |
| imports Main | |
| begin | |
| definition leftPad :: "'a ⇒ nat ⇒ 'a list ⇒ 'a list" | |
| where "leftPad padChar targetLength s ≡ replicate (targetLength - length s) padChar @ s" | |
| definition isPadded :: "'a ⇒ 'a list ⇒ 'a list ⇒ bool" | |
| where "isPadded padChar unpadded padded ≡ ∃ n. set (take n padded) ⊆ { padChar } ∧ drop n padded = unpadded" |
| module Unique where | |
| -- I deal with naturals instead of integers. with a bit more effort, I could | |
| -- probably have parameterized this over any type with decidable equality. | |
| open import Data.Nat | |
| open import Data.Product | |
| open import Data.List hiding (any) | |
| open import Data.List.Any | |
| open import Relation.Nullary | |
| open import Relation.Binary.PropositionalEquality |
| module HillelVerificationProblems where | |
| open import Data.Nat | |
| open import Data.Nat.Properties.Simple using (+-right-identity; +-comm) | |
| open import Data.List | |
| open import Data.List.All | |
| open import Data.List.Properties | |
| open import Relation.Binary.PropositionalEquality | |
| -- NB. (a ∸ b) is saturating subtraction and (a ⊔ b) is max(a,b). |
