vplogic

package
v0.27.4 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Sep 8, 2024 License: GPL-3.0 Imports: 21 Imported by: 0

Documentation

Overview

Package vplogic provides the core logic for all of Verifpal, allowing it to be imported as a package for use within other software.

Index

Constants

This section is empty.

Variables

View Source 
var VerifHubScheduledShared bool

VerifHubScheduledShared is a global variable that tracks whether VerifHub submission has been enabled for this analysis.

Functions

func Coq 

func Coq(modelFile string) error

Coq translates a Verifpal model into a representation that fits into the Coq model of the Verifpal verification methodology.

func InfoMessage 

func InfoMessage(m string, t string, showAnalysis bool)

InfoMessage prints a Verifpal status message either in color or non-color format, depending on what is supported by the terminal.

func InfoMessageColor 

func InfoMessageColor(m string, t string, analysisCount int)

InfoMessageColor prints a Verifpal status message in color format.

func InfoMessageRegular 

func InfoMessageRegular(m string, t string, analysisCount int)

InfoMessageRegular prints a Verifpal status message in non-color format.

func JSON added in v0.17.6 

func JSON(request string) error

JSON processes JSON requests made to Verifpal via the Visual Studio Code extension.

func JSONPrettyDiagram added in v0.17.6 

func JSONPrettyDiagram(inputString string) error

JSONPrettyDiagram formats a Verifpal model into a sequence diagram and returns the result in JSON format.

func JSONPrettyPrint added in v0.17.6 

func JSONPrettyPrint(inputString string) error

JSONPrettyPrint pretty-prints a Verifpal model and returns the result in JSON format.

func JSONPrettyQuery added in v0.17.6 

func JSONPrettyQuery(inputString string) error

JSONPrettyQuery pretty-prints a Verifpal query expression and returns the result in JSON format.

func JSONPrettyValue added in v0.17.6 

func JSONPrettyValue(inputString string) error

JSONPrettyValue pretty-prints a Verifpal value expression and returns the result in JSON format.

func JSONPrincipalStates added in v0.17.6 

func JSONPrincipalStates(inputString string) error

JSONPrincipalStates returns the KnowledgeMap struct for a given model in JSON format.

func JSONVerify added in v0.17.6 

func JSONVerify(inputString string) error

JSONVerify returns the verification result of a Verifpal model in JSON format.

func OpenBrowser 

func OpenBrowser(url string) error

OpenBrowser opens a URI using the appropriate binding for the host operating system.

func Parse 

func Parse(filename string, b []byte, opts ...Option) (any, error)

Parse parses the data from b using filename as information in the error messages.

func ParseFile 

func ParseFile(filename string, opts ...Option) (i any, err error)

ParseFile parses the file identified by filename.

func ParseReader 

func ParseReader(filename string, r io.Reader, opts ...Option) (any, error)

ParseReader parses the data from r using filename as information in the error messages.

func PrettyDiagram added in v0.14.6 

func PrettyDiagram(m Model) (string, error)

PrettyDiagram generates a sequence diagram format based on a Verifpal model.

func PrettyModel added in v0.14.5 

func PrettyModel(m Model) (string, error)

PrettyModel pretty-prints a Verifpal model that has already been parsed into the Model struct.

func PrettyPrint 

func PrettyPrint(modelFile string) error

PrettyPrint pretty-prints a Verifpal model based on a model loaded from a file.

func Pv 

func Pv(modelFile string) error

Pv translates a Verifpal model into a ProVerif model.

func VerifHub 

func VerifHub(m Model, fileName string, resultsCode string) error

VerifHub submits the given Verifpal model to VerifHub by opening the user's browser with the formatted model submission URI.

Types

type AttackerState 

type AttackerState struct {
	Active         bool
	CurrentPhase   int
	Exhausted      bool
	Known          []*Value
	PrincipalState []*PrincipalState
}

AttackerState contains the attacker's state during model analysis. In what follows, Known and PrincipalState operate as related columns, i.e. the n'th slice element in each of them corresponds to the n'th slice element in the other:

  • Active tracks whether this is an active attacker.
  • CurrentPhase tracks the phase at which the analysis is currently occurring.
  • Known tracks the values learned by the attacker.
  • PrincipalState contains a snapshot of the principal's PrincipalState at the moment where the corresponding value in Known was learned by the attacker.

type Block 

type Block struct {
	Kind      string
	Principal Principal
	Message   Message
	Phase     Phase
}

Block represents a principal, message or phase declaration in a Verifpal model.

type Cloner added in v0.23.0 

type Cloner interface {
	Clone() any
}

Cloner is implemented by any value that has a Clone method, which returns a copy of the value. This is mainly used for types which are not passed by value (e.g map, slice, chan) or structs that contain such types.

This is used in conjunction with the global state feature to create proper copies of the state to allow the parser to properly restore the state in the case of backtracking.

type Constant 

type Constant struct {
	Name        string
	ID          valueEnum
	Guard       bool
	Fresh       bool
	Leaked      bool
	Declaration typesEnum
	Qualifier   typesEnum
}

Constant represents a constant expression: - Name indicates the name of the constant. - ID indicates an internal ID for the constant. - Guard indicates if this is a guarded constant. - Fresh indicates if this is a "fresh" (i.e. generated) constant. - Leaked indicates if this constant has been leaked. - Declaration indicates how the constant was declared. - Qualifier indicates the "knows" qualifier (eg. "private").

type DecomposeRule 

type DecomposeRule struct {
	HasRule bool
	Given   []int
	Reveal  int
	Filter  func(*Primitive, *Value, int) (*Value, bool)
}

DecomposeRule contains a primitive's DecomposeRule.

type Equation 

type Equation struct {
	Values []*Value
}

Equation represents an equation expression.

type Expression 

type Expression struct {
	Kind      typesEnum
	Qualifier typesEnum
	Constants []*Constant
	Assigned  *Value
}

Expression represents one of the following kinds of expressions: - "knows": `knows [qualifier] [constants]`, eg. "knows private x" - "generates": `generates [constants]`, eg. "generates x, y" - "assignment": `[constants] = [value]`, eg. "x, y = HKDF(a, b, c)" - "leaks": `leaks [constants]`, eg. "leaks x"

type KnowledgeMap 

type KnowledgeMap struct {
	Principals    []string
	PrincipalIDs  []principalEnum
	Constants     []*Constant
	Assigned      []*Value
	Creator       []principalEnum
	KnownBy       [][]map[principalEnum]principalEnum
	DeclaredAt    []int
	MaxDeclaredAt int
	Phase         [][]int
	MaxPhase      int
}

KnowledgeMap represents Verifpal's internal map of knowledge of the model. It is constructed at the very beginning before Verifpal analysis commences and after the model is checked to be parseable, sane and error-free. After it is created, the KnowledgeMap structure is never changed. In what follows, Constants, Assigned, Creator, KnownBy, DeclaredAt and Phase operate as related columns, i.e. the n'th slice element in each of them corresponds to the n'th slice element in the other. - Principals contains the names of all model principals. - Constants contains all the constants within the model. - Assigned represents the values to which constants are assigned. - Creator represents the name of the principal who first declared the constant. - KnownBy is a map documenting from whom each principal came to know the constant. - DeclaredAt documents how many messages had passed before the constant was declared. - MaxDeclaredAt documents the maximum possible value for DeclaredAt. - Phase documents at which phase the constant was declared. - MaxPhase documents the maximum possible phase in the model.

func JSONKnowledgeMap added in v0.17.6 

func JSONKnowledgeMap(inputString string) (*KnowledgeMap, error)

JSONKnowledgeMap returns the KnowledgeMap struct for a given model in JSON format.

type Message 

type Message struct {
	Sender    principalEnum
	Recipient principalEnum
	Constants []*Constant
}

Message represents a message declaration in a Verifpal model.

type Model 

type Model struct {
	FileName string
	Attacker string
	Blocks   []Block
	Queries  []Query
}

Model is the main parsed representation of the Verifpal model.

type MutationMap 

type MutationMap struct {
	Initialized    bool
	OutOfMutations bool
	Constants      []*Constant
	Mutations      [][]*Value
	Combination    []*Value
	DepthIndex     []int
}

MutationMap contains the map of mutations that the attacker plans to apply to a PrincipalState. In what follows, Constants, Mutations and Combination operate as related columns, i.e. the n'th slice element in each of them corresponds to the n'th slice element in the other:

  • Initialized tracks whether this MutationMap has been populated.
  • OutOfMutations tracks whether all of the mutations in this map have been applied to its corresponding PrincipalState.
  • Constants tracks the constant which will be mutated.
  • Mutations tracks the possible mutations for this constant in the PrincipalState.

Combination and DepthIndex are internal values to track the combinatorial state of the MutationMap.

type Option 

type Option func(*parser) Option

Option is a function that can set an option on the parser. It returns the previous setting as an Option.

func AllowInvalidUTF8 added in v0.23.0 

func AllowInvalidUTF8(b bool) Option

AllowInvalidUTF8 creates an Option to allow invalid UTF-8 bytes. Every invalid UTF-8 byte is treated as a utf8.RuneError (U+FFFD) by character class matchers and is matched by the any matcher. The returned matched value, c.text and c.offset are NOT affected.

The default is false.

func Debug 

func Debug(b bool) Option

Debug creates an Option to set the debug flag to b. When set to true, debugging information is printed to stdout while parsing.

The default is false.

func Entrypoint added in v0.23.0 

func Entrypoint(ruleName string) Option

Entrypoint creates an Option to set the rule name to use as entrypoint. The rule name must have been specified in the -alternate-entrypoints if generating the parser with the -optimize-grammar flag, otherwise it may have been optimized out. Passing an empty string sets the entrypoint to the first rule in the grammar.

The default is to start parsing at the first rule in the grammar.

func GlobalStore added in v0.23.0 

func GlobalStore(key string, value any) Option

GlobalStore creates an Option to set a key to a certain value in the globalStore.

func InitState added in v0.23.0 

func InitState(key string, value any) Option

InitState creates an Option to set a key to a certain value in the global "state" store.

func MaxExpressions added in v0.23.0 

func MaxExpressions(maxExprCnt uint64) Option

MaxExpressions creates an Option to stop parsing after the provided number of expressions have been parsed, if the value is 0 then the parser will parse for as many steps as needed (possibly an infinite number).

The default for maxExprCnt is 0.

func Memoize 

func Memoize(b bool) Option

Memoize creates an Option to set the memoize flag to b. When set to true, the parser will cache all results so each expression is evaluated only once. This guarantees linear parsing time even for pathological cases, at the expense of more memory and slower times for typical cases.

The default is false.

func Recover 

func Recover(b bool) Option

Recover creates an Option to set the recover flag to b. When set to true, this causes the parser to recover from panics and convert it to an error. Setting it to false can be useful while debugging to access the full stack trace.

The default is true.

func Statistics added in v0.23.0 

func Statistics(stats *Stats, choiceNoMatch string) Option

Statistics adds a user provided Stats struct to the parser to allow the user to process the results after the parsing has finished. Also the key for the "no match" counter is set.

Example usage: 

input := "input"
stats := Stats{}
_, err := Parse("input-file", []byte(input), Statistics(&stats, "no match"))
if err != nil {
    log.Panicln(err)
}
b, err := json.MarshalIndent(stats.ChoiceAltCnt, "", "  ")
if err != nil {
    log.Panicln(err)
}
fmt.Println(string(b))

type Phase 

type Phase struct {
	Number int
}

Phase represents a phase declaration in a Verifpal model.

type Primitive 

type Primitive struct {
	ID        primitiveEnum
	Arguments []*Value
	Output    int
	Check     bool
}

Primitive represents a primitive expression: - ID indicates the internal enum ID of the primitives. - Arguments indicates the arguments of the primitive. - Output indicates which output value of the primitive this copy should rewrite to (starts at 0). - Check indicates whether this has been a checked primitive.

type PrimitiveCoreSpec 

type PrimitiveCoreSpec struct {
	Name      string
	ID        primitiveEnum
	Arity     []int
	Output    []int
	HasRule   bool
	CoreRule  func(*Primitive) (bool, []*Value)
	Check     bool
	Explosive bool
}

PrimitiveCoreSpec contains the definition of a core primitive.

type PrimitiveSpec 

type PrimitiveSpec struct {
	Name            string
	ID              primitiveEnum
	Arity           []int
	Output          []int
	Decompose       DecomposeRule
	Recompose       RecomposeRule
	Rewrite         RewriteRule
	Rebuild         RebuildRule
	Check           bool
	Explosive       bool
	PasswordHashing []int
}

PrimitiveSpec contains the definition of a primitive.

type Principal 

type Principal struct {
	Name        string
	ID          principalEnum
	Expressions []Expression
}

Principal represents a principal declaration in a Verifpal model.

type PrincipalState 

type PrincipalState struct {
	Name          string
	ID            principalEnum
	Constants     []*Constant
	Assigned      []*Value
	Guard         []bool
	Known         []bool
	Wire          [][]principalEnum
	KnownBy       [][]map[principalEnum]principalEnum
	DeclaredAt    []int
	MaxDeclaredAt int
	Creator       []principalEnum
	Sender        []principalEnum
	Rewritten     []bool
	BeforeRewrite []*Value
	Mutated       []bool
	MutatableTo   [][]principalEnum
	BeforeMutate  []*Value
	Phase         [][]int
}

PrincipalState represents the discrete state of each principal in a model. Each principal has their own PrincipalState, which continuously may be mutated by the active attacker under a set of rules as analysis progresses. Verifpal generates a new PrincipalState for each principal at each stage of the analysis. In that follows, Constants, Assigned, Guard, Known, Wire, KnownBy, DeclaredAt, Creator, Sender, Rewritten, BeforeRewrite, Mutated, MutatableTo, BeforeMutate and Phase operate as related columns, i.e. the n'th slice element in each of them corresponds to the n'th slice element in the other.

  • Name contains the name of the principal for whom this PrincipalState belongs to.
  • Constants contains all the constants within the model.
  • Assigned represents the values to which constants are assigned. This may be mutated by the active attacker during analysis.
  • Guard represents whether this value was guarded when this principal received it.
  • Known represents whether this principal ever gains knowledge of this value.
  • Wire represents the list of principals who received this constant over the wire (as a message).
  • KnownBy is a map documenting from whom each principal came to know the constant.
  • DeclaredAt documents how many messages had passed before the constant was declared.
  • MaxDeclaredAt documents the maximum possible value for DeclaredAt.
  • Creator represents the name of the principal who first declared the constant.
  • Sender represents which principal it was who sent this constant to this principal.
  • Rewritten tracks whether this value could be rewritten (eg. from `DEC(k,ENC(k,m))` to `m`). The rewritten value is then stored in Assigned.
  • BeforeRewrite tracks the value before it was rewritten.
  • Mutated tracks whether this value could be mutated by the active attacker (eg. from `G^a` to `G^nil`). The mutated value is then stored in Assigned.
  • MutatableTo tracks the principal for whom it is possible for this value to ever be mutated.
  • BeforeMutate tracks the value before it was mutated.
  • Phase documents at which phase the constant was declared.

type PvTemplate 

type PvTemplate struct {
	Parameters func(string) string
	Types      func() string
	Constants  func(*KnowledgeMap, string) string
	CorePrims  func() string
	Prims      func() string
	Channels   func(*KnowledgeMap) string
	Queries    func(*KnowledgeMap, []Query) (string, error)
	TopLevel   func([]Block) string
}

PvTemplate is a structure that helps contain parts of the ProVerif model which may be generated by Verifpal.

type Query 

type Query struct {
	Kind      typesEnum
	Constants []*Constant
	Message   Message
	Options   []QueryOption
}

Query represents a query declaration in a Verifpal model.

type QueryOption 

type QueryOption struct {
	Kind    typesEnum
	Message Message
}

QueryOption represents a query option (i.e. precondition) declaration in a Verifpal model.

type QueryOptionResult 

type QueryOptionResult struct {
	Option   QueryOption
	Resolved bool
	Summary  string
}

QueryOptionResult represents the analysis result of a QueryOption.

type RebuildRule 

type RebuildRule struct {
	HasRule bool
	ID      primitiveEnum
	Given   [][]int
	Reveal  int
	Filter  func(*Primitive, *Value, int) (*Value, bool)
}

RebuildRule contains a primitive's RebuildRule.

type RecomposeRule 

type RecomposeRule struct {
	HasRule bool
	Given   [][]int
	Reveal  int
	Filter  func(*Primitive, *Value, int) (*Value, bool)
}

RecomposeRule contains a primitive's RecomposeRule.

type RewriteRule 

type RewriteRule struct {
	HasRule  bool
	ID       primitiveEnum
	From     int
	To       func(*Primitive) *Value
	Matching map[int][]int
	Filter   func(*Primitive, *Value, int) (*Value, bool)
}

RewriteRule contains a primitive's RewriteRule.

type Stats added in v0.23.0 

type Stats struct {
	// ExprCnt counts the number of expressions processed during parsing
	// This value is compared to the maximum number of expressions allowed
	// (set by the MaxExpressions option).
	ExprCnt uint64

	// ChoiceAltCnt is used to count for each ordered choice expression,
	// which alternative is used how may times.
	// These numbers allow to optimize the order of the ordered choice expression
	// to increase the performance of the parser
	//
	// The outer key of ChoiceAltCnt is composed of the name of the rule as well
	// as the line and the column of the ordered choice.
	// The inner key of ChoiceAltCnt is the number (one-based) of the matching alternative.
	// For each alternative the number of matches are counted. If an ordered choice does not
	// match, a special counter is incremented. The name of this counter is set with
	// the parser option Statistics.
	// For an alternative to be included in ChoiceAltCnt, it has to match at least once.
	ChoiceAltCnt map[string]map[string]int
}

Stats stores some statistics, gathered during parsing

type Value 

type Value struct {
	Kind typesEnum
	Data interface{}
}

Value represents either a constant, primitive or equation expression.

type VerifyResult 

type VerifyResult struct {
	Query    Query
	Resolved bool
	Summary  string
	Options  []QueryOptionResult
}

VerifyResult contains the verification results for a particular query.

func Verify 

func Verify(filePath string) ([]VerifyResult, string, error)

Verify runs the main verification engine for Verifpal on a model loaded from a file. It returns a slice of verifyResults and a "results code".

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.