Kotlin conversion: Syntax checking

pgpainless-core/src/main/kotlin/org/pgpainless/decryption_verification/syntax_check/InputSymbol.kt

@@ -0,0 +1,39 @@
+// SPDX-FileCopyrightText: 2023 Paul Schaub <vanitasvitae@fsfe.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.pgpainless.decryption_verification.syntax_check
+
+enum class InputSymbol {
+    /**
+     * A [PGPLiteralData] packet.
+     */
+    LiteralData,
+    /**
+     * A [PGPSignatureList] object.
+     */
+    Signature,
+    /**
+     * A [PGPOnePassSignatureList] object.
+     */
+    OnePassSignature,
+    /**
+     * A [PGPCompressedData] packet.
+     * The contents of this packet MUST form a valid OpenPGP message, so a nested PDA is opened to verify
+     * its nested packet sequence.
+     */
+    CompressedData,
+    /**
+     * A [PGPEncryptedDataList] object.
+     * This object combines multiple ESKs and the corresponding Symmetrically Encrypted
+     * (possibly Integrity Protected) Data packet.
+     */
+    EncryptedData,
+    /**
+     * Marks the end of a (sub-) sequence.
+     * This input is given if the end of an OpenPGP message is reached.
+     * This might be the case for the end of the whole ciphertext, or the end of a packet with nested contents
+     * (e.g. the end of a Compressed Data packet).
+     */
+    EndOfSequence
+}

pgpainless-core/src/main/kotlin/org/pgpainless/decryption_verification/syntax_check/OpenPgpMessageSyntax.kt

@@ -0,0 +1,88 @@
+// SPDX-FileCopyrightText: 2023 Paul Schaub <vanitasvitae@fsfe.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.pgpainless.decryption_verification.syntax_check
+
+import org.pgpainless.exception.MalformedOpenPgpMessageException
+
+/**
+ * This class describes the syntax for OpenPGP messages as specified by rfc4880.
+ *
+ * See [rfc4880 - §11.3. OpenPGP Messages](https://www.rfc-editor.org/rfc/rfc4880#section-11.3)
+ * See [Blog post about theoretic background and translation of grammar to PDA syntax](https://blog.jabberhead.tk/2022/09/14/using-pushdown-automata-to-verify-packet-sequences/)
+ * See [Blog post about practically implementing the PDA for packet syntax validation](https://blog.jabberhead.tk/2022/10/26/implementing-packet-sequence-validation-using-pushdown-automata/)
+ */
+class OpenPgpMessageSyntax : Syntax {
+
+    override fun transition(from: State, input: InputSymbol, stackItem: StackSymbol?): Transition {
+        return when (from) {
+            State.OpenPgpMessage -> fromOpenPgpMessage(input, stackItem)
+            State.LiteralMessage -> fromLiteralMessage(input, stackItem)
+            State.CompressedMessage -> fromCompressedMessage(input, stackItem)
+            State.EncryptedMessage -> fromEncryptedMessage(input, stackItem)
+            State.Valid -> fromValid(input, stackItem)
+            else -> throw MalformedOpenPgpMessageException(from, input, stackItem)
+        }
+    }
+
+    fun fromOpenPgpMessage(input: InputSymbol, stackItem: StackSymbol?): Transition {
+        if (stackItem !== StackSymbol.msg) {
+            throw MalformedOpenPgpMessageException(State.OpenPgpMessage, input, stackItem)
+        }
+        return when (input) {
+            InputSymbol.LiteralData -> Transition(State.LiteralMessage)
+            InputSymbol.Signature -> Transition(State.OpenPgpMessage, StackSymbol.msg)
+            InputSymbol.OnePassSignature -> Transition(State.OpenPgpMessage, StackSymbol.ops, StackSymbol.msg)
+            InputSymbol.CompressedData -> Transition(State.CompressedMessage)
+            InputSymbol.EncryptedData -> Transition(State.EncryptedMessage)
+            InputSymbol.EndOfSequence -> throw MalformedOpenPgpMessageException(State.OpenPgpMessage, input, stackItem)
+            else -> throw MalformedOpenPgpMessageException(State.OpenPgpMessage, input, stackItem)
+        }
+    }
+
+    @Throws(MalformedOpenPgpMessageException::class)
+    fun fromLiteralMessage(input: InputSymbol, stackItem: StackSymbol?): Transition {
+        if (input == InputSymbol.Signature && stackItem == StackSymbol.ops) {
+            return Transition(State.LiteralMessage)
+        }
+        if (input == InputSymbol.EndOfSequence && stackItem == StackSymbol.terminus) {
+            return Transition(State.Valid)
+        }
+
+        throw MalformedOpenPgpMessageException(State.LiteralMessage, input, stackItem)
+    }
+
+    @Throws(MalformedOpenPgpMessageException::class)
+    fun fromCompressedMessage(input: InputSymbol, stackItem: StackSymbol?): Transition {
+        if (input == InputSymbol.Signature && stackItem == StackSymbol.ops) {
+            return Transition(State.CompressedMessage)
+        }
+        if (input == InputSymbol.EndOfSequence && stackItem == StackSymbol.terminus) {
+            return Transition(State.Valid)
+        }
+
+        throw MalformedOpenPgpMessageException(State.CompressedMessage, input, stackItem)
+    }
+
+    @Throws(MalformedOpenPgpMessageException::class)
+    fun fromEncryptedMessage(input: InputSymbol, stackItem: StackSymbol?): Transition {
+        if (input == InputSymbol.Signature && stackItem == StackSymbol.ops) {
+            return Transition(State.EncryptedMessage)
+        }
+        if (input == InputSymbol.EndOfSequence && stackItem == StackSymbol.terminus) {
+            return Transition(State.Valid)
+        }
+
+        throw MalformedOpenPgpMessageException(State.EncryptedMessage, input, stackItem)
+    }
+
+    @Throws(MalformedOpenPgpMessageException::class)
+    fun fromValid(input: InputSymbol, stackItem: StackSymbol?): Transition {
+        if (input == InputSymbol.EndOfSequence) {
+            // allow subsequent read() calls.
+            return Transition(State.Valid)
+        }
+        throw MalformedOpenPgpMessageException(State.Valid, input, stackItem)
+    }
+}

pgpainless-core/src/main/kotlin/org/pgpainless/decryption_verification/syntax_check/StackSymbol.kt

@@ -0,0 +1,20 @@
+// SPDX-FileCopyrightText: 2023 Paul Schaub <vanitasvitae@fsfe.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.pgpainless.decryption_verification.syntax_check
+
+enum class StackSymbol {
+    /**
+     * OpenPGP Message.
+     */
+    msg,
+    /**
+     * OnePassSignature (in case of BC this represents a OnePassSignatureList).
+     */
+    ops,
+    /**
+     * Special symbol representing the end of the message.
+     */
+    terminus
+}

pgpainless-core/src/main/kotlin/org/pgpainless/decryption_verification/syntax_check/State.kt

@@ -0,0 +1,16 @@
+// SPDX-FileCopyrightText: 2023 Paul Schaub <vanitasvitae@fsfe.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.pgpainless.decryption_verification.syntax_check
+
+/**
+ * Set of states of the automaton.
+ */
+enum class State {
+    OpenPgpMessage,
+    LiteralMessage,
+    CompressedMessage,
+    EncryptedMessage,
+    Valid
+}

pgpainless-core/src/main/kotlin/org/pgpainless/decryption_verification/syntax_check/Syntax.kt

@@ -0,0 +1,30 @@
+// SPDX-FileCopyrightText: 2023 Paul Schaub <vanitasvitae@fsfe.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.pgpainless.decryption_verification.syntax_check
+
+import org.pgpainless.exception.MalformedOpenPgpMessageException
+
+/**
+ * This interface can be used to define a custom syntax for the [PDA].
+ */
+interface Syntax {
+
+    /**
+     * Describe a transition rule from [State] <pre>from</pre> for [InputSymbol] <pre>input</pre>
+     * with [StackSymbol] <pre>stackItem</pre> from the top of the [PDAs][PDA] stack.
+     * The resulting [Transition] contains the new [State], as well as a list of
+     * [StackSymbols][StackSymbol] that get pushed onto the stack by the transition rule.
+     * If there is no applicable rule, a [MalformedOpenPgpMessageException] is thrown, since in this case
+     * the [InputSymbol] must be considered illegal.
+     *
+     * @param from current state of the PDA
+     * @param input input symbol
+     * @param stackItem item that got popped from the top of the stack
+     * @return applicable transition rule containing the new state and pushed stack symbols
+     * @throws MalformedOpenPgpMessageException if there is no applicable transition rule (the input symbol is illegal)
+     */
+    @Throws(MalformedOpenPgpMessageException::class)
+    fun transition(from: State, input: InputSymbol, stackItem: StackSymbol?): Transition
+}

pgpainless-core/src/main/kotlin/org/pgpainless/decryption_verification/syntax_check/Transition.kt

@@ -0,0 +1,22 @@
+// SPDX-FileCopyrightText: 2023 Paul Schaub <vanitasvitae@fsfe.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.pgpainless.decryption_verification.syntax_check
+
+/**
+ * Result of applying a transition rule.
+ * Transition rules can be described by implementing the [Syntax] interface.
+ *
+ * @param newState new [State] that is reached by applying the transition.
+ * @param pushedItems list of [StackSymbol] that are pushed onto the stack by applying the transition.
+ * The list contains items in the order in which they are pushed onto the stack.
+ * The list may be empty.
+ */
+class Transition private constructor(
+        val pushedItems: List<StackSymbol>,
+        val newState: State
+) {
+
+    constructor(newState: State, vararg pushedItems: StackSymbol): this(pushedItems.toList(), newState)
+}