lorchrob.github.io/index.html at master · lorchrob/lorchrob.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
<!DOCTYPE html>
<html>
<head>
  <meta charset="utf-8">
  <title>Rob Lorch</title>
  <link rel="stylesheet" href="style.css">
</head>

<body>

<img src="photo.jpeg" alt="Rob Lorch" class="photo">

<pre>

Rob Lorch
---------

PhD Candidate, Computer Science @ UIowa

Research Interests:
  - Automated reasoning
  - Computer security

Email:
  robert-lorch@uiowa.edu

Links:
  <a href="https://scholar.google.com/citations?hl=en&user=k9886iUAAAAJ&view_op=list_works&sortby=pubdate" target="_blank">Google Scholar</a>
  <a href="./cv.pdf" target="_blank">CV</a>
  <a href="https://github.com/lorchrob" target="_blank">GitHub</a>

About
-----

I'm a fourth-year computer science PhD candidate at the University of Iowa, where I am a member of the <a href="https://clc.cs.uiowa.edu/site/" target="_blank">Computational Logic Center</a>. I work under the supervision of <a href="https://homepage.cs.uiowa.edu/~tinelli/" target="_blank">Dr. Cesare Tinelli</a> and <a href="https://www3.cs.stonybrook.edu/~omar/" target="_blank">Dr. Omar Chowdhury</a> (@ Stony Brook University).

Broadly speaking, I am interested in automated techniques for detecting security vulnerabilities in computational systems, or proving their absence. In my work, I employ and develop tools and techniques from the field of automated reasoning (including SMT solving, model checking, deductive verification, logic programming, and so on).

Publications
------------

<b>ICSE '26.</b> <b>R. Lorch</b>, D. Dar, C. Tinelli, and O. Chowdhury, "Parse this! Summoning Context-Sensitive Inputs with Goblin" [<a href="./papers/goblin.pdf" target="_blank">pdf</a>]
^
In this paper, I develop a new approach for context-sensitive input generation (i.e., given a context-sensitive grammar G, find x such that x \in G). Such an input generation tool can be used to help fuzz software with complex inputs (e.g. pdf parsers), as one can encode the input specification as a context-sensitive grammar and then use the tool to generate system inputs. We applied this approach in [<a href="./papers/saecred.pdf" target="_blank">S&P '25</a>] (see below) to help discover security vulnerabilities in a widely-used implementation of the Wi-Fi SAE handshake protocol.

<b>Systems Engineering '26.</b> B. Meng, <b>R. Lorch</b>, K. Siu, M. Durling, S. Varanasi, S. Paul, and A. Moitra, "Transforming Natural Language Requirements to Formalism Using LLMs" [<a href="./papers/nl2f.pdf" target="_blank">pdf</a>]

<b>S&P '25.</b> D. Dar, <b>R. Lorch</b>, A. Sadeghi, V. Sorcigli, H. Gollier, C. Tinelli, M. Vanhoef, and O. Chowdhury, "SAECRED: A State-Aware, Over-the-Air Protocol Testing Approach for Discovering Parsing Bugs in SAE Handshake Implementations of COTS Wi-Fi Access Points" [<a href="./papers/saecred.pdf" target="_blank">pdf</a>]

<b>NFM '25.</b> B. Meng, S. Varanasi, <b>R. Lorch</b>, A. Moitra, K. Siu, S. Paul, M. Durling, N. Beniwal and N. Visnevski, "TRACE: Toolkit for Requirements Analysis Capture and Elicitation" [<a href="./papers/trace.pdf" target="_blank">pdf</a>]

<b>RAID '24.</b> <b>R. Lorch</b>, D. Larraz, C. Tinelli, and O. Chowdhury, "A Comprehensive, Automated Security Analysis of the Uptane Automotive Over-the-Air Update Framework" [<a href="./papers/uptane.pdf" target="_blank">pdf</a>]
^
In this paper, I explore novel techniques for interoperation between cryptographic protocol verifiers (e.g., Tamarin) and general-purpose model checkers (e.g., Kind 2) aimed towards the discovery of design-level vulnerabilities in security protocols.

<b>FormaliSE '24.</b> <b>R. Lorch</b>, B. Meng, K. Siu, A. Moitra, M. Durling, S. Paul, S. Varanasi, and C. McMillan, "Formal Methods in Requirements Engineering: Survey and Future Directions" [<a href="./papers/formalise.pdf" target="_blank">pdf</a>]

<b>FMCAD '23.</b> D. Larraz, <b>R. Lorch</b>, M. Yahyazadeh, F. Arif, O. Chowdhury, and C. Tinelli, "CRV: Automated Cyber-Resiliency Reasoning for System Design Models" [<a href="./papers/crv.pdf" target="_blank">pdf</a>]

<b>Australasian Journal of Combinatorics '22.</b> B. Carrigan, D. Diaz, J. Hammer, J. Lorch, and <b>R. Lorch</b>, "Constructing (3, b)-sudoku pair Latin squares" [<a href="./papers/ajc.pdf" target="_blank">pdf</a>]

<b>Bulletin of the Institute of Combinatorics and its Applications '21.</b> B. Carrigan, J. Hammer, J. Lorch, <b>R. Lorch</b>, and C. Owens, "List colorings count rokudoku-pair squares" [<a href="./papers/bica.pdf" target="_blank">pdf</a>]

Teaching
--------

Below is a list of courses I have taught in various capacities.

* UIowa Teaching Assistant
  [CS:4420, Spring '22] Artificial Intelligence
  [CS:5810, Fall '21] Formal Methods in Software Engineering
  [CS:2640, Fall '21] Computer Organization

* Grinnell College Class Mentor
  [CSC-207, Spring '21] Object-oriented data structures and algorithms

* Grinnell College Peer Tutor
  [CSC-161, Spring '21] Imperative problem solving and data structures

</pre>
</body>
</html>