Skip to content

Instantly share code, notes, and snippets.

View whitequark's full-sized avatar
🐈‍⬛

Catherine whitequark

🐈‍⬛
View GitHub Profile

General architecture for a hardware model checking tool

Key Principles

  • Things should feel real time
    • Solvers should be able to communicate between threads rapidly for clause sharing, solver shutdown etc
    • Main thread should be only used for comms between/launching threads, UI/user scripts should run in their own thread so you don't get the case where e.g. you can't load a CEX while a script is running
  • Users should have the power to control proof performance in sound and intuitive
@ryancdotorg
ryancdotorg / wzip.py
Last active April 8, 2024 14:20
Partial/streaming zip downloader
#!/usr/bin/env python3
# SPDX-License-Identifier: 0BSD or CC0-1.0 or MIT-0 or Unlicense
# Copyright (c) 2023, Ryan Castellucci, No Rights Reserved
import io, sys
import datetime
import argparse
import requests
import operator
import struct
@dev-zzo
dev-zzo / imperfect-design.md
Last active April 19, 2024 11:29
A curated list of research papers and blog posts on embedded security, keyed by the device p/n

The list below is compiled to inform, guide, and inspire budding security researchers. Oh and to pick something for bedtime reading too.

Included in the list are works on the following topics related to MCU/SoC security:

  • Secure boot
  • Fault injection
  • Side channel attacks

At the end of the list, there is also a section with links to articles of potential general interest, not addressing vulnerabilities in any specific device.

Foreward

This document was originally written several years ago. At the time I was working as an execution core verification engineer at Arm. The following points are coloured heavily by working in and around the execution cores of various processors. Apply a pinch of salt; points contain varying degrees of opinion.

It is still my opinion that RISC-V could be much better designed; though I will also say that if I was building a 32 or 64-bit CPU today I'd likely implement the architecture to benefit from the existing tooling.

Mostly based upon the RISC-V ISA spec v2.0. Some updates have been made for v2.2

Original Foreword: Some Opinion

The RISC-V ISA has pursued minimalism to a fault. There is a large emphasis on minimizing instruction count, normalizing encoding, etc. This pursuit of minimalism has resulted in false orthogonalities (such as reusing the same instruction for branches, calls and returns) and a requirement for superfluous instructions which impacts code density both in terms of size and

@porglezomp
porglezomp / twitter-alt-to-title.user.js
Last active March 16, 2022 15:43
Copy the alt text in tweets into the title text, so that you can see it on hover.
// ==UserScript==
// @name Twitter Alt-Text to Title-Text
// @description Copy the alt attribute of twitter images into the title attribute, so that I can see the alt text on hover.
// @version 1
// @grant none
// @include https://twitter.com/*
// ==/UserScript==
const SELECTORS = `.tweet .AdaptiveMedia-photoContainer img
, .Gallery-media img
#!/usr/bin/env python3
import sys
import textwrap
# Very basic bitstream to SVF converter, tested with the ULX3S WiFi interface
flash_page_size = 256
erase_block_size = 64*1024
@smunaut
smunaut / ice40_global.md
Last active May 5, 2020 14:18
iCE40 Global Networks

UP5k SG48:

ID Use SB_IO_GB SB_GB Special
x/y/z (pin) x/y x/y type
0 Clk / Reset 19/ 0/1 (20) 13/ 0
1 Clk / CE 6/ 0/1 (44) 13/31
2 Clk / Reset 13/31/0 (37) 19/31 12/31 PLL_B
3 Clk / CE 6/31
#!/usr/bin/env python3
with open("vbmeta.img", "rb+") as vbmeta:
# Get current flags
vbmeta.seek(123)
flags = int.from_bytes(vbmeta.read(1), byteorder='big')
# Disable verity
flags |= 0x01
# Disable verification
flags |= 0x02
@marcan
marcan / ghettohci.c
Created April 24, 2018 16:48
GhettOHCI - perhaps the world's smallest and stupidest OHCI stack.
/*
mini - a Free Software replacement for the Nintendo/BroadOn IOS.
ghettohci - debug over FT232 over OHCI
Copyright (C) 2012 Hector Martin "marcan" <marcan@marcansoft.com>
# This code is licensed to you under the terms of the GNU GPL, version 2;
# see file COPYING or http://www.gnu.org/licenses/old-licenses/gpl-2.0.txt
*/
@pdn4kd
pdn4kd / topics.md
Last active March 9, 2023 22:45 — forked from eggrobin/topics.md
#kspacademia topicquotes

The conversation that led to the creation of the channel:

<ferram4|afk> So, I continue following references on supersonic wing stuff,
and I find a paper that tries to tweak linear supersonic flow to work for
high AoA, hypersonic flight.
<KinglyRedLion> the FUCK
<ferram4|afk> I love technical papers. ^_^
<KinglyRedLion> Why would you do high AOA hypersonic?
<egg|zzz|egg> KinglyRedLion: to publish