[K] AWS security issue

[nrryuya]

Because of this K's issue, we remove kprove tests from CI for now.

Copied from RV's public channel.

patrick.mackay [9:24 PM]
Good Morning - Runtime Verification recently identified a security issue with respect to its AWS console.  We are taking steps to identify and address this issue. As a result, you may see disruption to work related to the K-ecosystem.  We apologize in advance for any and all disruption to your work.  Rest assured we are diligently working as quickly as possible to have everything back up and running.  We will provide updates as they become available.

The current error.

git clone https://github.com/kframework/k .build/k
Cloning into '.build/k'...
remote: Enumerating objects: 1729, done.        
remote: Counting objects: 100% (1729/1729), done.        
remote: Compressing objects: 100% (738/738), done.        
remote: Total 213548 (delta 700), reused 1603 (delta 627), pack-reused 211819        
Receiving objects: 100% (213548/213548), 52.87 MiB | 33.56 MiB/s, done.
Resolving deltas: 100% (122383/122383), done.
cd .build/k \
    && git reset --hard b65568ade007d54dd21667f4f56f2d7471bb6596 \
    && mvn package -DskipTests
HEAD is now at b65568ade Logging: minor fix.
[INFO] Scanning for projects...
Downloading from runtime.verification.snapshots: https://s3.amazonaws.com/repo.runtime.verification/repository/snapshots/com/runtimeverification/rv_match/parent/1.0-SNAPSHOT/maven-metadata.xml
[WARNING] Could not transfer metadata com.runtimeverification.rv_match:parent:1.0-SNAPSHOT/maven-metadata.xml from/to runtime.verification.snapshots (https://s3.amazonaws.com/repo.runtime.verification/repository/snapshots): Access denied to: https://s3.amazonaws.com/repo.runtime.verification/repository/snapshots/com/runtimeverification/rv_match/parent/1.0-SNAPSHOT/maven-metadata.xml , ReasonPhrase:Forbidden.
Downloading from runtime.verification.snapshots: https://s3.amazonaws.com/repo.runtime.verification/repository/snapshots/com/runtimeverification/rv_match/parent/1.0-SNAPSHOT/parent-1.0-SNAPSHOT.pom
[ERROR] [ERROR] Some problems were encountered while processing the POMs:
[FATAL] Non-resolvable parent POM for com.runtimeverification.k:parent:[unknown-version]: Could not transfer artifact com.runtimeverification.rv_match:parent:pom:1.0-SNAPSHOT from/to runtime.verification.snapshots (https://s3.amazonaws.com/repo.runtime.verification/repository/snapshots): Access denied to: https://s3.amazonaws.com/repo.runtime.verification/repository/snapshots/com/runtimeverification/rv_match/parent/1.0-SNAPSHOT/parent-1.0-SNAPSHOT.pom , ReasonPhrase:Forbidden. and 'parent.relativePath' points at wrong local POM @ line 5, column 11
 @ 
[ERROR] The build could not read 1 project -> [Help 1]
[ERROR]   
[ERROR]   The project com.runtimeverification.k:parent:[unknown-version] (/root/verified-vyper-contracts/k/.build/k/pom.xml) has 1 error
[ERROR]     Non-resolvable parent POM for com.runtimeverification.k:parent:[unknown-version]: Could not transfer artifact com.runtimeverification.rv_match:parent:pom:1.0-SNAPSHOT from/to runtime.verification.snapshots (https://s3.amazonaws.com/repo.runtime.verification/repository/snapshots): Access denied to: https://s3.amazonaws.com/repo.runtime.verification/repository/snapshots/com/runtimeverification/rv_match/parent/1.0-SNAPSHOT/parent-1.0-SNAPSHOT.pom , ReasonPhrase:Forbidden. and 'parent.relativePath' points at wrong local POM @ line 5, column 11 -> [Help 2]
[ERROR] 
[ERROR] To see the full stack trace of the errors, re-run Maven with the -e switch.
[ERROR] Re-run Maven using the -X switch to enable full debug logging.
[ERROR] 
[ERROR] For more information about the errors and possible solutions, please read the following articles:
[ERROR] [Help 1] http://cwiki.apache.org/confluence/display/MAVEN/ProjectBuildingException
[ERROR] [Help 2] http://cwiki.apache.org/confluence/display/MAVEN/UnresolvableModelException
Makefile:30: recipe for target 'k' failed
make: *** [k] Error 1

[nrryuya]

patrick.mackay [9:01 PM]
- update: we have addressed the issue with AWS and we are operational again. Thank you for your patience. Our apologies again for the disruption to your work. Have a great week.

[yudetamago]

At least, it seems to be necessary to skip llvm build ( https://github.com/kframework/evm-semantics/commit/465a97e15099ba1f7b6b27698fd23fd6d835b3ce ) and update k commit hash to 25e358c3a2cb9fa0156fbb81077eaeb88b24d689 or later (https://github.com/kframework/k/commit/25e358c3a2cb9fa0156fbb81077eaeb88b24d689 ) but after that, building process successes and proving some specs fails...

[nrryuya]

@yudetamago Thanks!

proving some specs fails

All specs fail? or some specs pass?

[yudetamago]

@nrryuya

All specs fail? or some specs pass?

The latter.

For example in ERC20 spec, allowance-spec.k and totalSupply-spec.k pass but approve-spec.k, transferFrom-success-2-spec.k and transfer-success-2-spec.k cause the following error. (with 25e358c3a2cb9fa0156fbb81077eaeb88b24d689 k commit hash )

Initialization finished
==================================
Total time:            27.560
  Parsing time:        25.779
  Initialization time: 1.781
  Execution time:      0.000

Init+Execution time:    1.781
  query build time:     0.035 s
  Z3 constraint time:  0.000 s
  Z3 implication time:  0.603 s
    Z3 implication queries:   30
  resolveFunction time: 1.661 s
resolveFunction top-level calls:   8514
==================================

[Error] Internal: Uncaught exception thrown of type AssertionError.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues (null)
make: *** [specs/ERC20/transferFrom-success-2-spec.k.test] Error 1

[nrryuya]

The cause might be this issue. Could you retry with BYZANTIUM? https://github.com/kframework/evm-semantics/issues/287

[yudetamago]

ah, I'll try that 👍

[yudetamago]

BYZANTIUM works 😉