issues
search
viperproject
/
VerifiedSCION
Verifying the SCION architecture using Gobra
Apache License 2.0
10
stars
2
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
add missing 'ghost'
#377
jcp19
opened
3 days ago
0
Fix failing CI due to outdated upload action
#376
jcp19
closed
3 days ago
0
Scripts
#375
Dspil
opened
3 days ago
0
Move ownership of underlying slice of `SerializableBuffer` to outside of `Mem()`
#374
mlimbeck
closed
2 weeks ago
2
packSCMP Continued
#373
mlimbeck
closed
1 month ago
1
make `hf_valid` opaque
#372
jcp19
closed
1 month ago
0
processEpic Continued
#371
mlimbeck
closed
2 weeks ago
1
Stabilize `path/scion`
#370
jcp19
closed
2 weeks ago
0
Drop IO-assumptions in processOHP
#369
mlimbeck
closed
1 month ago
0
Drop SetHopfield related assumptions
#368
mlimbeck
closed
2 months ago
0
Reenable chopper in the CI
#367
jcp19
opened
2 months ago
0
Drop two assumptions and merge validity criteria `StronglyValid` and `FullyValid`
#366
jcp19
closed
2 months ago
0
Merge criteria `StronglyValid()` and `FullyValid()` for `scion.Base`
#365
jcp19
closed
2 months ago
0
Strengthen `parsePath` and drop two temporary assumptions related to SCION issues
#364
jcp19
closed
2 months ago
0
Drop assumptions of `IsSupportedPkt` in `process`
#363
mlimbeck
closed
2 months ago
0
Simplify specs of decodeLayers
#362
jcp19
opened
2 months ago
0
Proof of SetHopField
#361
mlimbeck
closed
4 weeks ago
2
Finish `prepareSCMP`
#360
jcp19
opened
2 months ago
1
Format `info_hop_setter_lemmas.gobra`
#359
jcp19
closed
2 months ago
0
Drop explicit underlying buffer parameters
#358
jcp19
opened
3 months ago
0
`path`: Make Len impure and add LenSpec
#357
jcp19
closed
3 months ago
0
Simplification of segLens
#356
mlimbeck
closed
3 months ago
0
Reformat, drop `/*@`/`@*/` blocks to ensure consistent styling...
#355
jcp19
closed
3 months ago
0
Clean-up and renaming of `AbsSlice_Bytes`
#354
jcp19
closed
3 months ago
0
Readability improvements
#353
jcp19
opened
3 months ago
0
Simplify validity criteria of paths
#352
jcp19
closed
2 months ago
0
Formatting in the `router`
#351
jcp19
closed
3 months ago
0
Drop Assumption in SetInfoField
#350
mlimbeck
closed
3 months ago
3
Fix ghostness of output params
#349
jcp19
closed
3 months ago
0
Drop assumption in parsePath
#348
mlimbeck
closed
3 months ago
0
major simplification in paths
#347
jcp19
closed
3 months ago
0
Simplify path/scion
#346
jcp19
closed
3 months ago
0
Verify assumptions in SCION.DecodeFromBytes
#345
mlimbeck
closed
3 months ago
0
Proof of incPath
#344
mlimbeck
closed
4 months ago
0
Use Z3 API
#343
jcp19
closed
3 months ago
0
[will not merge] Don't assume injectivity on inhale
#342
jcp19
closed
4 months ago
0
Refactoring of absPkt
#341
mlimbeck
closed
4 months ago
0
Enable `conditionalizePermissions` for the `router`
#340
jcp19
closed
4 months ago
0
Drop `trusted` annotation in method
#339
jcp19
closed
4 months ago
0
Introduce obligations to enforce closing locks
#338
jcp19
opened
4 months ago
0
Use Gobra's built-in ghost fields
#337
jcp19
closed
3 months ago
0
[will no merge] Check where things fail if we drop requirement based on `InfForHfSpec`
#336
jcp19
closed
4 months ago
0
bring changes from #243
#335
jcp19
closed
4 months ago
0
IO-spec lemmas
#334
mlimbeck
closed
4 months ago
0
Proof of Internal Packet Bouncing fix (#4502)
#333
mlimbeck
closed
4 months ago
1
router: forbid bouncing packets internally (#4502)
#332
jcp19
closed
4 months ago
0
[Experiment] Disable MCE
#331
jcp19
closed
4 months ago
0
change triggers in absPktWidenLemma
#330
Dspil
closed
4 months ago
0
fix assumed termination measure
#329
jcp19
closed
4 months ago
0
Enable chop 10 in the CI of the router
#328
jcp19
closed
4 months ago
0
Next